#NAME part71.
Term : Type.
lam : (Term -> Term) -> Term.
def app : Term -> Term -> Term.
(; beta-reduction ;)
[f,t] app (lam f) t --> f t.
type : Type.
arrow : type -> type -> type.
def term : type -> Type.
[A,B] term (arrow A B) --> term A -> term B.
def fix : A : type -> B : type ->
((term A -> term B) -> term A -> term B) ->
term A -> term B.
[A,B,F,a] fix A B F a --> F (fix A B F) a.
nat : type.
def Nat := term nat.
O : Nat.
S : Nat -> Nat.
def match_nat : Nat -> Nat -> (Nat -> Nat) -> Nat.
[n0,nS] match_nat O n0 nS --> n0
[n,n0,nS] match_nat (S n) n0 nS --> nS n.
def mod2 := fix nat nat
(m2 => n =>
match_nat n
O
(p => match_nat p
(S O)
(q => m2 q))).
#CONV mod2 (S (S (S (S O)))), O.