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)