DEFINITION minus_Sx_Sy()
TYPE =
       ∀x:nat.∀y:nat.(eq nat (minus (S x) (S y)) (minus x y))
BODY =
        assume x: nat
        assume y: nat
          by (refl_equal . .)
          we proved eq nat (minus x y) (minus x y)
          that is equivalent to eq nat (minus (S x) (S y)) (minus x y)
       we proved ∀x:nat.∀y:nat.(eq nat (minus (S x) (S y)) (minus x y))