DEFINITION r_dis()
TYPE =
       ∀k:K
         .∀P:Prop
           .(∀i:nat.(eq nat (r k i) i))→P
             →((∀i:nat.(eq nat (r k i) (S i)))→P)→P
BODY =
       assume k: K
          we proceed by induction on k to prove 
             ∀P:Prop
               .(∀i:nat.(eq nat (r k i) i))→P
                 →((∀i:nat.(eq nat (r k i) (S i)))→P)→P
             case Bind : b:B ⇒
                the thesis becomes 
                ∀P:Prop
                  .∀H:(∀i:nat.(eq nat (r (Bind b) i) i))→P
                    .((∀i:nat.(eq nat (r (Bind b) i) (S i)))→P)→P
                    assume P: Prop
                    suppose H: (∀i:nat.(eq nat (r (Bind b) i) i))→P
                    suppose : (∀i:nat.(eq nat (r (Bind b) i) (S i)))→P
                      assume i: nat
                         by (refl_equal . .)
                         we proved eq nat i i
                         that is equivalent to eq nat (r (Bind b) i) i
                      we proved ∀i:nat.(eq nat (r (Bind b) i) i)
                      by (H previous)
                      we proved P

                      ∀P:Prop
                        .∀H:(∀i:nat.(eq nat (r (Bind b) i) i))→P
                          .((∀i:nat.(eq nat (r (Bind b) i) (S i)))→P)→P
             case Flat : f:F ⇒
                the thesis becomes 
                ∀P:Prop
                  .(∀i:nat.(eq nat (r (Flat f) i) i))→P
                    →∀H0:(∀i:nat.(eq nat (r (Flat f) i) (S i)))→P.P
                    assume P: Prop
                    suppose : (∀i:nat.(eq nat (r (Flat f) i) i))→P
                    suppose H0: (∀i:nat.(eq nat (r (Flat f) i) (S i)))→P
                      assume i: nat
                         by (refl_equal . .)
                         we proved eq nat (S i) (S i)
                         that is equivalent to eq nat (r (Flat f) i) (S i)
                      we proved ∀i:nat.(eq nat (r (Flat f) i) (S i))
                      by (H0 previous)
                      we proved P

                      ∀P:Prop
                        .(∀i:nat.(eq nat (r (Flat f) i) i))→P
                          →∀H0:(∀i:nat.(eq nat (r (Flat f) i) (S i)))→P.P
          we proved 
             ∀P:Prop
               .(∀i:nat.(eq nat (r k i) i))→P
                 →((∀i:nat.(eq nat (r k i) (S i)))→P)→P
       we proved 
          ∀k:K
            .∀P:Prop
              .(∀i:nat.(eq nat (r k i) i))→P
                →((∀i:nat.(eq nat (r k i) (S i)))→P)→P