DEFINITION minus_s_s()
TYPE =
       ∀k:K.∀i:nat.∀j:nat.(eq nat (minus (s k i) (s k j)) (minus i j))
BODY =
       assume k: K
          we proceed by induction on k to prove ∀i:nat.∀j:nat.(eq nat (minus (s k i) (s k j)) (minus i j))
             case Bind : :B ⇒
                the thesis becomes ∀i:nat.∀j:nat.(eq nat (minus i j) (minus i j))
                    assume i: nat
                    assume j: nat
                      by (refl_equal . .)
                      we proved eq nat (minus i j) (minus i j)
                      that is equivalent to eq nat (minus (s (Bind __3) i) (s (Bind __3) j)) (minus i j)
∀i:nat.∀j:nat.(eq nat (minus i j) (minus i j))
             case Flat : :F ⇒
                the thesis becomes ∀i:nat.∀j:nat.(eq nat (minus i j) (minus i j))
                    assume i: nat
                    assume j: nat
                      by (refl_equal . .)
                      we proved eq nat (minus i j) (minus i j)
                      that is equivalent to eq nat (minus (s (Flat __3) i) (s (Flat __3) j)) (minus i j)
∀i:nat.∀j:nat.(eq nat (minus i j) (minus i j))
          we proved ∀i:nat.∀j:nat.(eq nat (minus (s k i) (s k j)) (minus i j))
       we proved ∀k:K.∀i:nat.∀j:nat.(eq nat (minus (s k i) (s k j)) (minus i j))