DEFINITION pr2_gen_cflat()
TYPE =
       ∀f:F.∀c:C.∀v:T.∀t1:T.∀t2:T.(pr2 (CHead c (Flat f) v) t1 t2)→(pr2 c t1 t2)
BODY =
        assume f: F
        assume c: C
        assume v: T
        assume t1: T
        assume t2: T
        suppose H: pr2 (CHead c (Flat f) v) t1 t2
           assume y: C
           suppose H0: pr2 y t1 t2
             we proceed by induction on H0 to prove (eq C y (CHead c (Flat f) v))→(pr2 c t1 t2)
                case pr2_free : c0:C t3:T t4:T H1:pr0 t3 t4 ⇒
                   the thesis becomes (eq C c0 (CHead c (Flat f) v))→(pr2 c t3 t4)
                      suppose : eq C c0 (CHead c (Flat f) v)
                         by (pr2_free . . . H1)
                         we proved pr2 c t3 t4
(eq C c0 (CHead c (Flat f) v))→(pr2 c t3 t4)
                case pr2_delta : c0:C d:C u:T i:nat H1:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H2:pr0 t3 t4 t:T H3:subst0 i u t4 t ⇒
                   the thesis becomes ∀H4:(eq C c0 (CHead c (Flat f) v)).(pr2 c t3 t)
                      suppose H4: eq C c0 (CHead c (Flat f) v)
                         (H5) 
                            we proceed by induction on H4 to prove getl i (CHead c (Flat f) v) (CHead d (Bind Abbr) u)
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H1
getl i (CHead c (Flat f) v) (CHead d (Bind Abbr) u)
                         end of H5
                         (H_y) 
                            by (getl_gen_flat . . . . . H5)
getl i c (CHead d (Bind Abbr) u)
                         end of H_y
                         by (pr2_delta . . . . H_y . . H2 . H3)
                         we proved pr2 c t3 t
∀H4:(eq C c0 (CHead c (Flat f) v)).(pr2 c t3 t)
             we proved (eq C y (CHead c (Flat f) v))→(pr2 c t1 t2)
          we proved ∀y:C.(pr2 y t1 t2)→(eq C y (CHead c (Flat f) v))→(pr2 c t1 t2)
          by (insert_eq . . . . previous H)
          we proved pr2 c t1 t2
       we proved ∀f:F.∀c:C.∀v:T.∀t1:T.∀t2:T.(pr2 (CHead c (Flat f) v) t1 t2)→(pr2 c t1 t2)