DEFINITION getl_gen_sort()
TYPE =
       ∀n:nat.∀h:nat.∀x:C.(getl h (CSort n) x)→∀P:Prop.P
BODY =
        assume n: nat
        assume h: nat
        assume x: C
        suppose H: getl h (CSort n) x
        assume P: Prop
          (H0) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop h O (CSort n) e λe:C.clear e x
          end of H0
          we proceed by induction on H0 to prove P
             case ex_intro2 : x0:C H1:drop h O (CSort n) x0 H2:clear x0 x ⇒
                the thesis becomes P
                   by (drop_gen_sort . . . . H1)
                   we proved and3 (eq C x0 (CSort n)) (eq nat h O) (eq nat O O)
                   we proceed by induction on the previous result to prove P
                      case and3_intro : H3:eq C x0 (CSort n) :eq nat h O :eq nat O O ⇒
                         the thesis becomes P
                            (H6) 
                               we proceed by induction on H3 to prove clear (CSort n) x
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H2
clear (CSort n) x
                            end of H6
                            by (clear_gen_sort . . H6 .)
P
P
          we proved P
       we proved ∀n:nat.∀h:nat.∀x:C.(getl h (CSort n) x)→∀P:Prop.P