DEFINITION s_minus()
TYPE =
       ∀k:K
         .∀i:nat
           .∀j:nat.(le j i)→(eq nat (s k (minus i j)) (minus (s k i) j))
BODY =
       assume k: K
          we proceed by induction on k to prove 
             ∀i:nat
               .∀j:nat.(le j i)→(eq nat (s k (minus i j)) (minus (s k i) j))
             case Bind : :B ⇒
                the thesis becomes ∀i:nat.∀j:nat.∀H:(le j i).(eq nat (S (minus i j)) (minus (S i) j))
                    assume i: nat
                    assume j: nat
                    suppose H: le j i
                      (h1) 
                         by (refl_equal . .)
eq nat (minus (S i) j) (minus (S i) j)
                      end of h1
                      (h2) 
                         by (minus_Sn_m . . H)
eq nat (S (minus i j)) (minus (S i) j)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved eq nat (S (minus i j)) (minus (S i) j)
                      that is equivalent to eq nat (s (Bind __4) (minus i j)) (minus (s (Bind __4) i) j)
∀i:nat.∀j:nat.∀H:(le j i).(eq nat (S (minus i j)) (minus (S i) j))
             case Flat : f:F ⇒
                the thesis becomes 
                ∀i:nat
                  .∀j:nat
                    .le j i
                      →eq nat (minus (s (Flat f) i) j) (minus (s (Flat f) i) j)
                    assume i: nat
                    assume j: nat
                    suppose : le j i
                      by (refl_equal . .)
                      we proved eq nat (minus (s (Flat f) i) j) (minus (s (Flat f) i) j)
                      that is equivalent to eq nat (s (Flat f) (minus i j)) (minus (s (Flat f) i) j)

                      ∀i:nat
                        .∀j:nat
                          .le j i
                            →eq nat (minus (s (Flat f) i) j) (minus (s (Flat f) i) j)
          we proved 
             ∀i:nat
               .∀j:nat.(le j i)→(eq nat (s k (minus i j)) (minus (s k i) j))
       we proved 
          ∀k:K
            .∀i:nat
              .∀j:nat.(le j i)→(eq nat (s k (minus i j)) (minus (s k i) j))