DEFINITION csubst1_getl_ge()
TYPE =
       ∀i:nat
         .∀n:nat.(le i n)→∀c1:C.∀c2:C.∀v:T.(csubst1 i v c1 c2)→∀e:C.(getl n c1 e)→(getl n c2 e)
BODY =
        assume i: nat
        assume n: nat
        suppose H: le i n
        assume c1: C
        assume c2: C
        assume v: T
        suppose H0: csubst1 i v c1 c2
          we proceed by induction on H0 to prove ∀e:C.(getl n c1 e)→(getl n c2 e)
             case csubst1_refl : ⇒
                the thesis becomes ∀e:C.(getl n c1 e)→(getl n c1 e)
                    assume e: C
                    suppose H1: getl n c1 e
                      consider H1
∀e:C.(getl n c1 e)→(getl n c1 e)
             case csubst1_sing : c3:C H1:csubst0 i v c1 c3 ⇒
                the thesis becomes ∀e:C.∀H2:(getl n c1 e).(getl n c3 e)
                    assume e: C
                    suppose H2: getl n c1 e
                      by (csubst0_getl_ge . . H . . . H1 . H2)
                      we proved getl n c3 e
∀e:C.∀H2:(getl n c1 e).(getl n c3 e)
          we proved ∀e:C.(getl n c1 e)→(getl n c2 e)
       we proved 
          ∀i:nat
            .∀n:nat.(le i n)→∀c1:C.∀c2:C.∀v:T.(csubst1 i v c1 c2)→∀e:C.(getl n c1 e)→(getl n c2 e)