DEFINITION minus_plus()
TYPE =
       ∀n:nat.∀m:nat.(eq nat (minus (plus n m) n) m)
BODY =
        assume n: nat
        assume m: nat
          by (refl_equal . .)
          we proved eq nat (plus n m) (plus n m)
          by (plus_minus . . . previous)
          we proved eq nat m (minus (plus n m) n)
          by (sym_eq . . . previous)
          we proved eq nat (minus (plus n m) n) m
       we proved ∀n:nat.∀m:nat.(eq nat (minus (plus n m) n) m)