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

(provide eq-symm eq-trans)

(define eq-symm
 '(? : (∀ (S : Type) -> (∀ (x : S) -> (∀ (y : S) -> ((x = y) -> (y = x)))))))

(define eq-trans
  '(? : (∀ (S : Type) -> (∀ (x : S) -> (∀ (y : S) -> (∀ (z : S) ->
            ((x = y) -> ((y = z) -> (x = z)))))))))