DEFINITION r_minus()
TYPE =
       ∀i:nat
         .∀n:nat
           .lt n i
             →∀k:K.(eq nat (minus (r k i) (S n)) (r k (minus i (S n))))
BODY =
        assume i: nat
        assume n: nat
        suppose H: lt n i
        assume k: K
          we proceed by induction on k to prove eq nat (minus (r k i) (S n)) (r k (minus i (S n)))
             case Bind : :B ⇒
                the thesis becomes 
                eq
                  nat
                  minus (r (Bind __1) i) (S n)
                  r (Bind __1) (minus i (S n))
                   by (refl_equal . .)
                   we proved eq nat (minus i (S n)) (minus i (S n))

                      eq
                        nat
                        minus (r (Bind __1) i) (S n)
                        r (Bind __1) (minus i (S n))
             case Flat : :F ⇒
                the thesis becomes 
                eq
                  nat
                  minus (r (Flat __1) i) (S n)
                  r (Flat __1) (minus i (S n))
                   by (minus_x_Sy . . H)
                   we proved eq nat (minus i n) (S (minus i (S n)))

                      eq
                        nat
                        minus (r (Flat __1) i) (S n)
                        r (Flat __1) (minus i (S n))
          we proved eq nat (minus (r k i) (S n)) (r k (minus i (S n)))
       we proved 
          ∀i:nat
            .∀n:nat
              .lt n i
                →∀k:K.(eq nat (minus (r k i) (S n)) (r k (minus i (S n))))