DEFINITION getl_mono()
TYPE =
       ∀c:C.∀x1:C.∀h:nat.(getl h c x1)→∀x2:C.(getl h c x2)→(eq C x1 x2)
BODY =
        assume c: C
        assume x1: C
        assume h: nat
        suppose H: getl h c x1
        assume x2: C
        suppose H0: getl h c x2
          (H1) 
             by (getl_gen_all . . . H0)
ex2 C λe:C.drop h O c e λe:C.clear e x2
          end of H1
          we proceed by induction on H1 to prove eq C x1 x2
             case ex_intro2 : x:C H2:drop h O c x H3:clear x x2 ⇒
                the thesis becomes eq C x1 x2
                   (H4) 
                      by (getl_gen_all . . . H)
ex2 C λe:C.drop h O c e λe:C.clear e x1
                   end of H4
                   we proceed by induction on H4 to prove eq C x1 x2
                      case ex_intro2 : x0:C H5:drop h O c x0 H6:clear x0 x1 ⇒
                         the thesis becomes eq C x1 x2
                            (H7) 
                               by (drop_mono . . . . H2 . H5)
                               we proved eq C x x0
                               we proceed by induction on the previous result to prove drop h O c x0
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H2
drop h O c x0
                            end of H7
                            (H9) 
                               by (drop_mono . . . . H2 . H5)
                               we proved eq C x x0
                               by (eq_ind_r . . . H6 . previous)
clear x x1
                            end of H9
                            by (clear_mono . . H9 . H3)
eq C x1 x2
eq C x1 x2
          we proved eq C x1 x2
       we proved ∀c:C.∀x1:C.∀h:nat.(getl h c x1)→∀x2:C.(getl h c x2)→(eq C x1 x2)