105def naturalEqual =
106 (lambda unrestricted left : Nat .
107 (lambda unrestricted right : Nat .
108 (nat-eliminate (lambda unrestricted current : Nat . Nat)
109 (nat-eliminate (lambda unrestricted current : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero)) (nat-less-than left right))
110 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
111 (nat-less-than right left))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.