DEFINITION pr2_head_1()
TYPE =
       ∀c:C.∀u1:T.∀u2:T.(pr2 c u1 u2)→∀k:K.∀t:T.(pr2 c (THead k u1 t) (THead k u2 t))
BODY =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pr2 c u1 u2
        assume k: K
        assume t: T
          we proceed by induction on H to prove pr2 c (THead k u1 t) (THead k u2 t)
             case pr2_free : c0:C t1:T t2:T H0:pr0 t1 t2 ⇒
                the thesis becomes pr2 c0 (THead k t1 t) (THead k t2 t)
                   by (pr0_refl .)
                   we proved pr0 t t
                   by (pr0_comp . . H0 . . previous .)
                   we proved pr0 (THead k t1 t) (THead k t2 t)
                   by (pr2_free . . . previous)
pr2 c0 (THead k t1 t) (THead k t2 t)
             case pr2_delta : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) t1:T t2:T H1:pr0 t1 t2 t0:T H2:subst0 i u t2 t0 ⇒
                the thesis becomes pr2 c0 (THead k t1 t) (THead k t0 t)
                   (h1) 
                      by (pr0_refl .)
                      we proved pr0 t t
                      by (pr0_comp . . H1 . . previous .)
pr0 (THead k t1 t) (THead k t2 t)
                   end of h1
                   (h2) 
                      by (subst0_fst . . . . H2 . .)
subst0 i u (THead k t2 t) (THead k t0 t)
                   end of h2
                   by (pr2_delta . . . . H0 . . h1 . h2)
pr2 c0 (THead k t1 t) (THead k t0 t)
          we proved pr2 c (THead k u1 t) (THead k u2 t)
       we proved ∀c:C.∀u1:T.∀u2:T.(pr2 c u1 u2)→∀k:K.∀t:T.(pr2 c (THead k u1 t) (THead k u2 t))