44def sm86NaturalSubtract =
45 (lambda unrestricted left : Nat .
46 (lambda unrestricted right : Nat .
47 (nat-eliminate
48 (lambda unrestricted current : Nat . Nat)
49 left
50 (lambda unrestricted predecessor : Nat .
51 (lambda unrestricted induction : Nat . (sm86NaturalPredecessor induction)))
52 right)))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.