DEFINITION pr2_cflat()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→∀f:F.∀v:T.(pr2 (CHead c (Flat f) v) t1 t2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr2 c t1 t2
        assume f: F
        assume v: T
          we proceed by induction on H to prove pr2 (CHead c (Flat f) v) t1 t2
             case pr2_free : c0:C t3:T t4:T H0:pr0 t3 t4 ⇒
                the thesis becomes pr2 (CHead c0 (Flat f) v) t3 t4
                   by (pr2_free . . . H0)
pr2 (CHead c0 (Flat f) v) t3 t4
             case pr2_delta : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H1:pr0 t3 t4 t:T H2:subst0 i u t4 t ⇒
                the thesis becomes pr2 (CHead c0 (Flat f) v) t3 t
                   by (getl_flat . . . H0 . .)
                   we proved getl i (CHead c0 (Flat f) v) (CHead d (Bind Abbr) u)
                   by (pr2_delta . . . . previous . . H1 . H2)
pr2 (CHead c0 (Flat f) v) t3 t
          we proved pr2 (CHead c (Flat f) v) t1 t2
       we proved ∀c:C.∀t1:T.∀t2:T.(pr2 c t1 t2)→∀f:F.∀v:T.(pr2 (CHead c (Flat f) v) t1 t2)