DEFINITION pr3_wcpr0_t()
TYPE =
∀c1:C.∀c2:C.(wcpr0 c2 c1)→∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pr3 c2 t1 t2)
BODY =
assume c1: C
assume c2: C
suppose H: wcpr0 c2 c1
we proceed by induction on H to prove ∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pr3 c2 t1 t2)
case wcpr0_refl : c:C ⇒
assume t1: T
assume t2: T
suppose H0: pr3 c t1 t2
consider H0
case wcpr0_comp : c0:C c3:C H0:wcpr0 c0 c3 u1:T u2:T H2:pr0 u1 u2 k:K ⇒
the thesis becomes ∀t1:T.∀t2:T.∀H3:(pr3 (CHead c3 k u2) t1 t2).(pr3 (CHead c0 k u1) t1 t2)
() by induction hypothesis we know ∀t1:T.∀t2:T.(pr3 c3 t1 t2)→(pr3 c0 t1 t2)
assume t1: T
assume t2: T
suppose H3: pr3 (CHead c3 k u2) t1 t2
by (pr2_free . . . H2)
we proved pr2 c3 u1 u2
by (pr3_pr2_pr3_t . . . . . H3 . previous)
we proved pr3 (CHead c3 k u1) t1 t2
we proceed by induction on the previous result to prove pr3 (CHead c0 k u1) t1 t2
case pr3_refl : t:T ⇒
the thesis becomes pr3 (CHead c0 k u1) t t
by (pr3_refl . .)
pr3 (CHead c0 k u1) t t
case pr3_sing : t0:T t3:T H4:pr2 (CHead c3 k u1) t3 t0 t4:T :pr3 (CHead c3 k u1) t0 t4 ⇒
the thesis becomes pr3 (CHead c0 k u1) t3 t4
(H6) by induction hypothesis we know pr3 (CHead c0 k u1) t0 t4
assume y: C
suppose H7: pr2 y t3 t0
we proceed by induction on H7 to prove (eq C y (CHead c3 k u1))→(pr3 (CHead c0 k u1) t3 t0)
case pr2_free : c:C t5:T t6:T H8:pr0 t5 t6 ⇒
the thesis becomes (eq C c (CHead c3 k u1))→(pr3 (CHead c0 k u1) t5 t6)
suppose : eq C c (CHead c3 k u1)
by (pr2_free . . . H8)
we proved pr2 (CHead c0 k u1) t5 t6
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c0 k u1) t5 t6
(eq C c (CHead c3 k u1))→(pr3 (CHead c0 k u1) t5 t6)
case pr2_delta : c:C d:C u:T i:nat H8:getl i c (CHead d (Bind Abbr) u) t5:T t6:T H9:pr0 t5 t6 t:T H10:subst0 i u t6 t ⇒
the thesis becomes ∀H11:(eq C c (CHead c3 k u1)).(pr3 (CHead c0 k u1) t5 t)
suppose H11: eq C c (CHead c3 k u1)
(H12)
we proceed by induction on H11 to prove getl i (CHead c3 k u1) (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H8
getl i (CHead c3 k u1) (CHead d (Bind Abbr) u)
end of H12
by (pr0_refl .)
we proved pr0 u1 u1
by (wcpr0_comp . . H0 . . previous .)
we proved wcpr0 (CHead c0 k u1) (CHead c3 k u1)
by (wcpr0_getl_back . . previous . . . . H12)
we proved
ex3_2 C T λe2:C.λu2:T.getl i (CHead c0 k u1) (CHead e2 (Bind Abbr) u2) λe2:C.λ:T.wcpr0 e2 d λ:C.λu2:T.pr0 u2 u
we proceed by induction on the previous result to prove pr3 (CHead c0 k u1) t5 t
case ex3_2_intro : x0:C x1:T H13:getl i (CHead c0 k u1) (CHead x0 (Bind Abbr) x1) :wcpr0 x0 d H15:pr0 x1 u ⇒
the thesis becomes pr3 (CHead c0 k u1) t5 t
by (pr0_subst0_back . . . . H10 . H15)
we proved ex2 T λt:T.subst0 i x1 t6 t λt:T.pr0 t t
we proceed by induction on the previous result to prove pr3 (CHead c0 k u1) t5 t
case ex_intro2 : x:T H16:subst0 i x1 t6 x H17:pr0 x t ⇒
the thesis becomes pr3 (CHead c0 k u1) t5 t
(h1)
by (pr2_delta . . . . H13 . . H9 . H16)
pr2 (CHead c0 k u1) t5 x
end of h1
(h2)
by (pr2_free . . . H17)
we proved pr2 (CHead c0 k u1) x t
by (pr3_pr2 . . . previous)
pr3 (CHead c0 k u1) x t
end of h2
by (pr3_sing . . . h1 . h2)
pr3 (CHead c0 k u1) t5 t
pr3 (CHead c0 k u1) t5 t
we proved pr3 (CHead c0 k u1) t5 t
∀H11:(eq C c (CHead c3 k u1)).(pr3 (CHead c0 k u1) t5 t)
we proved (eq C y (CHead c3 k u1))→(pr3 (CHead c0 k u1) t3 t0)
we proved ∀y:C.(pr2 y t3 t0)→(eq C y (CHead c3 k u1))→(pr3 (CHead c0 k u1) t3 t0)
by (insert_eq . . . . previous H4)
we proved pr3 (CHead c0 k u1) t3 t0
by (pr3_t . . . previous . H6)
pr3 (CHead c0 k u1) t3 t4
we proved pr3 (CHead c0 k u1) t1 t2
∀t1:T.∀t2:T.∀H3:(pr3 (CHead c3 k u2) t1 t2).(pr3 (CHead c0 k u1) t1 t2)
we proved ∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pr3 c2 t1 t2)
we proved ∀c1:C.∀c2:C.(wcpr0 c2 c1)→∀t1:T.∀t2:T.(pr3 c1 t1 t2)→(pr3 c2 t1 t2)