#lang racket
;; Starter code for A6Q2
;; May contain Unicode characters - download, don't cut/paste from browser
;; You must replace the ? with correct proof terms.

(provide cong plus plus-zero-left plus-zero-right)

(define plus '(? : (Nat -> (Nat -> Nat))))

(define cong
  '(? : (∀ (A : Type) -> (∀ (B : Type)
         -> (∀ (x : A) -> (∀ (y : A) -> (∀ (f : (A -> B))
         -> ((x = y) -> ((f x) = (f y))))))))))

(define plus-zero-left
  '(? : (∀ (n : Nat) -> (((plus Z) n) = n))))

(define plus-zero-right
  '(? : (∀ (n : Nat) -> (((plus n) Z) = n))))