DEFINITION s_inj()
TYPE =
       ∀k:K.∀i:nat.∀j:nat.(eq nat (s k i) (s k j))→(eq nat i j)
BODY =
       assume k: K
          we proceed by induction on k to prove ∀i:nat.∀j:nat.(eq nat (s k i) (s k j))→(eq nat i j)
             case Bind : b:B ⇒
                the thesis becomes ∀i:nat.∀j:nat.∀H:(eq nat (s (Bind b) i) (s (Bind b) j)).(eq nat i j)
                    assume i: nat
                    assume j: nat
                    suppose H: eq nat (s (Bind b) i) (s (Bind b) j)
                      consider H
                      we proved eq nat (s (Bind b) i) (s (Bind b) j)
                      that is equivalent to eq nat (S i) (S j)
                      by (eq_add_S . . previous)
                      we proved eq nat i j
∀i:nat.∀j:nat.∀H:(eq nat (s (Bind b) i) (s (Bind b) j)).(eq nat i j)
             case Flat : f:F ⇒
                the thesis becomes 
                ∀i:nat
                  .∀j:nat
                    .∀H:eq nat (s (Flat f) i) (s (Flat f) j)
                      .eq nat (s (Flat f) i) (s (Flat f) j)
                    assume i: nat
                    assume j: nat
                    suppose H: eq nat (s (Flat f) i) (s (Flat f) j)
                      consider H
                      we proved eq nat (s (Flat f) i) (s (Flat f) j)
                      that is equivalent to eq nat i j

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