val plus : nat -> nat -> nat
= fn x => rec x
of p(0) => (fn y => y)
| p(s(x')) => (fn y => s(p(x') y))
end;
term refl : !x:nat. (x = x) =
fn x => rec x of
f 0 => eq0
| f (s x') => eqS (f x')
end;
term lmps : !x:nat. !y:nat. plus x (s y) = s (plus x y) =
fn x => rec x of
f 0 => fn y => refl (s y)
| f (s x') => fn y => eqS (f x' y)
end;
term trans : !x:nat. !y:nat. !z:nat. (x = y) => (y = z) => (x = z) =
fn x => rec x of
f 0 => fn y => rec y of
g 0 => fn z => fn p => fn q => q
| g (s y') => fn z => fn p => fn q => eqE0S p
end
| f (s x') => fn y => rec y of
g 0 => fn z => fn p => fn q => eqES0 p
| g (s y') => fn z => rec z of
h 0 => fn p => fn q => eqES0 q
| h (s z') => fn p => fn q => eqS (f x' y' z' (eqESS p) (eqESS q))
end
end
end;
term ev : !x:nat. (?y:nat. plus y y = x) | (?y:nat. s (plus y y) = x) =
fn x => rec x of
f 0 => inl (0, eq0)
| f (s x') => case f x' of
inl u => let (c, p) = u in inr (c, eqS p)
| inr w => let (d, q) = w in inl (s d,
trans (plus (s d) (s d)) (s (plus (s d) d)) (s x')
(lmps (s d) d) (eqS q))
end
end;
term pred' : !x:nat. ~(x = 0) => ?y:nat. s(y) = x =
fn x => rec x of
f 0 => fn u => (0, abort (u eq0))
| f (s x') => fn u => (x', refl (s x'))
end;