#lang racket
;; Starter code for A6Q4
;; May contain Unicode characters - download, don't cut/paste from browser
;; You must replace the ? with correct proof terms.
;; Marks will be assigned by hand; Marmoset just checks for valid definitions.

(provide even two-is-even)

(define even '(? : (Nat -> Type)))

(define two-is-even '(? : (even (S (S Z)))))