DEFINITION pc3_wcpr0__pc3_wcpr0_t_aux()
TYPE =
∀c1:C.∀c2:C.(wcpr0 c1 c2)→∀k:K.∀u:T.∀t1:T.∀t2:T.(pr3 (CHead c1 k u) t1 t2)→(pc3 (CHead c2 k u) t1 t2)
BODY =
assume c1: C
assume c2: C
suppose H: wcpr0 c1 c2
assume k: K
assume u: T
assume t1: T
assume t2: T
suppose H0: pr3 (CHead c1 k u) t1 t2
we proceed by induction on H0 to prove pc3 (CHead c2 k u) t1 t2
case pr3_refl : t:T ⇒
the thesis becomes pc3 (CHead c2 k u) t t
by (pc3_refl . .)
pc3 (CHead c2 k u) t t
case pr3_sing : t3:T t4:T H1:pr2 (CHead c1 k u) t4 t3 t5:T :pr3 (CHead c1 k u) t3 t5 ⇒
the thesis becomes pc3 (CHead c2 k u) t4 t5
(H3) by induction hypothesis we know pc3 (CHead c2 k u) t3 t5
assume y: C
suppose H4: pr2 y t4 t3
we proceed by induction on H4 to prove (eq C y (CHead c1 k u))→(pc3 (CHead c2 k u) t4 t3)
case pr2_free : c:C t6:T t0:T H5:pr0 t6 t0 ⇒
the thesis becomes (eq C c (CHead c1 k u))→(pc3 (CHead c2 k u) t6 t0)
suppose : eq C c (CHead c1 k u)
by (pr2_free . . . H5)
we proved pr2 (CHead c2 k u) t6 t0
by (pc3_pr2_r . . . previous)
we proved pc3 (CHead c2 k u) t6 t0
(eq C c (CHead c1 k u))→(pc3 (CHead c2 k u) t6 t0)
case pr2_delta : c:C d:C u0:T i:nat H5:getl i c (CHead d (Bind Abbr) u0) t6:T t0:T H6:pr0 t6 t0 t:T H7:subst0 i u0 t0 t ⇒
the thesis becomes ∀H8:(eq C c (CHead c1 k u)).(pc3 (CHead c2 k u) t6 t)
suppose H8: eq C c (CHead c1 k u)
(H9)
we proceed by induction on H8 to prove getl i (CHead c1 k u) (CHead d (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
getl i (CHead c1 k u) (CHead d (Bind Abbr) u0)
end of H9
by (pr0_refl .)
we proved pr0 u u
by (wcpr0_comp . . H . . previous .)
we proved wcpr0 (CHead c1 k u) (CHead c2 k u)
by (wcpr0_getl . . previous . . . . H9)
we proved
ex3_2 C T λe2:C.λu2:T.getl i (CHead c2 k u) (CHead e2 (Bind Abbr) u2) λe2:C.λ:T.wcpr0 d e2 λ:C.λu2:T.pr0 u0 u2
we proceed by induction on the previous result to prove pc3 (CHead c2 k u) t6 t
case ex3_2_intro : x0:C x1:T H10:getl i (CHead c2 k u) (CHead x0 (Bind Abbr) x1) :wcpr0 d x0 H12:pr0 u0 x1 ⇒
the thesis becomes pc3 (CHead c2 k u) t6 t
by (pr0_subst0_fwd . . . . H7 . H12)
we proved ex2 T λt:T.subst0 i x1 t0 t λt:T.pr0 t t
we proceed by induction on the previous result to prove pc3 (CHead c2 k u) t6 t
case ex_intro2 : x:T H13:subst0 i x1 t0 x H14:pr0 t x ⇒
the thesis becomes pc3 (CHead c2 k u) t6 t
(h1)
by (pr2_delta . . . . H10 . . H6 . H13)
pr2 (CHead c2 k u) t6 x
end of h1
(h2)
by (pr2_free . . . H14)
we proved pr2 (CHead c2 k u) t x
by (pc3_pr2_x . . . previous)
pc3 (CHead c2 k u) x t
end of h2
by (pc3_pr2_u . . . h1 . h2)
pc3 (CHead c2 k u) t6 t
pc3 (CHead c2 k u) t6 t
we proved pc3 (CHead c2 k u) t6 t
∀H8:(eq C c (CHead c1 k u)).(pc3 (CHead c2 k u) t6 t)
we proved (eq C y (CHead c1 k u))→(pc3 (CHead c2 k u) t4 t3)
we proved ∀y:C.(pr2 y t4 t3)→(eq C y (CHead c1 k u))→(pc3 (CHead c2 k u) t4 t3)
by (insert_eq . . . . previous H1)
we proved pc3 (CHead c2 k u) t4 t3
by (pc3_t . . . previous . H3)
pc3 (CHead c2 k u) t4 t5
we proved pc3 (CHead c2 k u) t1 t2
we proved ∀c1:C.∀c2:C.(wcpr0 c1 c2)→∀k:K.∀u:T.∀t1:T.∀t2:T.(pr3 (CHead c1 k u) t1 t2)→(pc3 (CHead c2 k u) t1 t2)