DEFINITION pr3_pr3_pr3_t()
TYPE =
       ∀c:C.∀u1:T.∀u2:T.(pr3 c u1 u2)→∀t1:T.∀t2:T.∀k:K.(pr3 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)
BODY =
        assume c: C
        assume u1: T
        assume u2: T
        suppose H: pr3 c u1 u2
          we proceed by induction on H to prove ∀t1:T.∀t2:T.∀k:K.(pr3 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)
             case pr3_refl : t:T ⇒
                    assume t1: T
                    assume t2: T
                    assume k: K
                    suppose H0: pr3 (CHead c k t) t1 t2
                      consider H0
             case pr3_sing : t2:T t1:T H0:pr2 c t1 t2 t3:T :pr3 c t2 t3 ⇒
                the thesis becomes ∀t0:T.∀t4:T.∀k:K.∀H3:(pr3 (CHead c k t3) t0 t4).(pr3 (CHead c k t1) t0 t4)
                (H2) by induction hypothesis we know ∀t4:T.∀t5:T.∀k:K.(pr3 (CHead c k t3) t4 t5)→(pr3 (CHead c k t2) t4 t5)
                    assume t0: T
                    assume t4: T
                    assume k: K
                    suppose H3: pr3 (CHead c k t3) t0 t4
                      by (H2 . . . H3)
                      we proved pr3 (CHead c k t2) t0 t4
                      by (pr3_pr2_pr3_t . . . . . previous . H0)
                      we proved pr3 (CHead c k t1) t0 t4
∀t0:T.∀t4:T.∀k:K.∀H3:(pr3 (CHead c k t3) t0 t4).(pr3 (CHead c k t1) t0 t4)
          we proved ∀t1:T.∀t2:T.∀k:K.(pr3 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)
       we proved ∀c:C.∀u1:T.∀u2:T.(pr3 c u1 u2)→∀t1:T.∀t2:T.∀k:K.(pr3 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)