DEFINITION pc3_pr2_pr2_t()
TYPE =
∀c:C.∀u1:T.∀u2:T.(pr2 c u2 u1)→∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)
BODY =
assume c: C
assume u1: T
assume u2: T
suppose H: pr2 c u2 u1
we proceed by induction on H to prove ∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)
case pr2_free : c0:C t1:T t2:T H0:pr0 t1 t2 ⇒
the thesis becomes ∀t0:T.∀t3:T.∀k:K.∀H1:(pr2 (CHead c0 k t1) t0 t3).(pc3 (CHead c0 k t2) t0 t3)
assume t0: T
assume t3: T
assume k: K
suppose H1: pr2 (CHead c0 k t1) t0 t3
by (pc3_pr0_pr2_t . . H0 . . . . H1)
we proved pc3 (CHead c0 k t2) t0 t3
∀t0:T.∀t3:T.∀k:K.∀H1:(pr2 (CHead c0 k t1) t0 t3).(pc3 (CHead c0 k t2) t0 t3)
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 t:T H2:subst0 i u t2 t ⇒
the thesis becomes ∀t0:T.∀t3:T.∀k:K.∀H3:(pr2 (CHead c0 k t1) t0 t3).(pc3 (CHead c0 k t) t0 t3)
assume t0: T
assume t3: T
assume k: K
suppose H3: pr2 (CHead c0 k t1) t0 t3
assume y: C
suppose H4: pr2 y t0 t3
we proceed by induction on H4 to prove (eq C y (CHead c0 k t1))→(pc3 (CHead c0 k t) t0 t3)
case pr2_free : c1:C t4:T t5:T H5:pr0 t4 t5 ⇒
the thesis becomes (eq C c1 (CHead c0 k t1))→(pc3 (CHead c0 k t) t4 t5)
suppose : eq C c1 (CHead c0 k t1)
by (pr2_free . . . H5)
we proved pr2 (CHead c0 k t) t4 t5
by (pc3_pr2_r . . . previous)
we proved pc3 (CHead c0 k t) t4 t5
(eq C c1 (CHead c0 k t1))→(pc3 (CHead c0 k t) t4 t5)
case pr2_delta : c1:C d0:C u0:T i0:nat H5:getl i0 c1 (CHead d0 (Bind Abbr) u0) t4:T t5:T H6:pr0 t4 t5 t6:T H7:subst0 i0 u0 t5 t6 ⇒
the thesis becomes ∀H8:(eq C c1 (CHead c0 k t1)).(pc3 (CHead c0 k t) t4 t6)
suppose H8: eq C c1 (CHead c0 k t1)
(H9)
we proceed by induction on H8 to prove getl i0 (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
getl i0 (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
end of H9
suppose H10: getl O (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
suppose H11: subst0 O u0 t5 t6
by (getl_gen_O . . H10)
we proved clear (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
assume b: B
suppose H12: clear (CHead c0 (Bind b) t1) (CHead d0 (Bind Abbr) u0)
(H13)
by (clear_gen_bind . . . . H12)
we proved eq C (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒d0 | CHead c2 ⇒c2
<λ:C.C> CASE CHead c0 (Bind b) t1 OF CSort ⇒d0 | CHead c2 ⇒c2
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d0 | CHead c2 ⇒c2 (CHead d0 (Bind Abbr) u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d0 | CHead c2 ⇒c2 (CHead c0 (Bind b) t1)
end of H13
(h1)
(H14)
by (clear_gen_bind . . . . H12)
we proved eq C (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d0 (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c0 (Bind b) t1 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead d0 (Bind Abbr) u0
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
CHead c0 (Bind b) t1
end of H14
(h1)
(H15)
by (clear_gen_bind . . . . H12)
we proved eq C (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒u0 | CHead t7⇒t7
<λ:C.T> CASE CHead c0 (Bind b) t1 OF CSort ⇒u0 | CHead t7⇒t7
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t7⇒t7 (CHead d0 (Bind Abbr) u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t7⇒t7 (CHead c0 (Bind b) t1)
end of H15
suppose H16: eq B Abbr b
suppose : eq C d0 c0
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒u0 | CHead t7⇒t7
<λ:C.T> CASE CHead c0 (Bind b) t1 OF CSort ⇒u0 | CHead t7⇒t7
that is equivalent to eq T u0 t1
we proceed by induction on the previous result to prove subst0 O t1 t5 t6
case refl_equal : ⇒
the thesis becomes the hypothesis H11
subst0 O t1 t5 t6
end of H18
we proceed by induction on H16 to prove pc3 (CHead c0 (Bind b) t) t4 t6
case refl_equal : ⇒
the thesis becomes pc3 (CHead c0 (Bind Abbr) t) t4 t6
by (pr0_subst0_fwd . . . . H18 . H1)
we proved ex2 T λt:T.subst0 O t2 t5 t λt:T.pr0 t6 t
we proceed by induction on the previous result to prove pc3 (CHead c0 (Bind Abbr) t) t4 t6
case ex_intro2 : x:T H19:subst0 O t2 t5 x H20:pr0 t6 x ⇒
the thesis becomes pc3 (CHead c0 (Bind Abbr) t) t4 t6
by (subst0_subst0_back . . . . H19 . . . H2)
we proved ex2 T λt:T.subst0 O t t5 t λt:T.subst0 (S (plus i O)) u x t
we proceed by induction on the previous result to prove pc3 (CHead c0 (Bind Abbr) t) t4 t6
case ex_intro2 : x0:T H21:subst0 O t t5 x0 H22:subst0 (S (plus i O)) u x x0 ⇒
the thesis becomes pc3 (CHead c0 (Bind Abbr) t) t4 t6
(H23)
by (plus_n_O .)
we proved eq nat i (plus i O)
by (sym_eq . . . previous)
we proved eq nat (plus i O) i
by (f_equal . . . . . previous)
eq nat (S (plus i O)) (S i)
end of H23
(H24)
we proceed by induction on H23 to prove subst0 (S i) u x x0
case refl_equal : ⇒
the thesis becomes the hypothesis H22
subst0 (S i) u x x0
end of H24
(h1)
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind Abbr) t) (CHead c0 (Bind Abbr) t)
by (pr2_delta . . . . previous . . H6 . H21)
pr2 (CHead c0 (Bind Abbr) t) t4 x0
end of h1
(h2)
consider H0
we proved getl i c0 (CHead d (Bind Abbr) u)
that is equivalent to getl (r (Bind Abbr) i) c0 (CHead d (Bind Abbr) u)
by (getl_head . . . . previous .)
we proved getl (S i) (CHead c0 (Bind Abbr) t) (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H20 . H24)
we proved pr2 (CHead c0 (Bind Abbr) t) t6 x0
by (pc3_pr2_x . . . previous)
pc3 (CHead c0 (Bind Abbr) t) x0 t6
end of h2
by (pc3_pr2_u . . . h1 . h2)
pc3 (CHead c0 (Bind Abbr) t) t4 t6
pc3 (CHead c0 (Bind Abbr) t) t4 t6
pc3 (CHead c0 (Bind Abbr) t) t4 t6
we proved pc3 (CHead c0 (Bind b) t) t4 t6
(eq B Abbr b)→(eq C d0 c0)→(pc3 (CHead c0 (Bind b) t) t4 t6)
end of h1
(h2)
consider H14
we proved
eq
B
<λ:C.B>
CASE CHead d0 (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c0 (Bind b) t1 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
eq B Abbr b
end of h2
by (h1 h2)
(eq C d0 c0)→(pc3 (CHead c0 (Bind b) t) t4 t6)
end of h1
(h2)
consider H13
we proved
eq
C
<λ:C.C> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒d0 | CHead c2 ⇒c2
<λ:C.C> CASE CHead c0 (Bind b) t1 OF CSort ⇒d0 | CHead c2 ⇒c2
eq C d0 c0
end of h2
by (h1 h2)
we proved pc3 (CHead c0 (Bind b) t) t4 t6
∀H12:clear (CHead c0 (Bind b) t1) (CHead d0 (Bind Abbr) u0)
.pc3 (CHead c0 (Bind b) t) t4 t6
assume f: F
suppose H12: clear (CHead c0 (Flat f) t1) (CHead d0 (Bind Abbr) u0)
(h1)
by (getl_refl . . .)
we proved getl O (CHead d0 (Bind Abbr) u0) (CHead d0 (Bind Abbr) u0)
by (pr2_delta . . . . previous . . H6 . H11)
we proved pr2 (CHead d0 (Bind Abbr) u0) t4 t6
by (pc3_pr2_r . . . previous)
pc3 (CHead d0 (Bind Abbr) u0) t4 t6
end of h1
(h2)
by (clear_gen_flat . . . . H12)
we proved clear c0 (CHead d0 (Bind Abbr) u0)
by (clear_flat . . previous . .)
clear (CHead c0 (Flat f) t) (CHead d0 (Bind Abbr) u0)
end of h2
by (clear_pc3_trans . . . h1 . h2)
we proved pc3 (CHead c0 (Flat f) t) t4 t6
∀H12:clear (CHead c0 (Flat f) t1) (CHead d0 (Bind Abbr) u0)
.pc3 (CHead c0 (Flat f) t) t4 t6
by (previous . previous)
we proved pc3 (CHead c0 k t) t4 t6
getl O (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
→(subst0 O u0 t5 t6)→(pc3 (CHead c0 k t) t4 t6)
assume i1: nat
suppose :
getl i1 (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
→(subst0 i1 u0 t5 t6)→(pc3 (CHead c0 k t) t4 t6)
suppose H10: getl (S i1) (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
suppose H11: subst0 (S i1) u0 t5 t6
by (getl_gen_S . . . . . H10)
we proved getl (r k i1) c0 (CHead d0 (Bind Abbr) u0)
assume b: B
suppose H12: getl (r (Bind b) i1) c0 (CHead d0 (Bind Abbr) u0)
by (getl_head . . . . H12 .)
we proved getl (S i1) (CHead c0 (Bind b) t) (CHead d0 (Bind Abbr) u0)
by (pr2_delta . . . . previous . . H6 . H11)
we proved pr2 (CHead c0 (Bind b) t) t4 t6
by (pc3_pr2_r . . . previous)
we proved pc3 (CHead c0 (Bind b) t) t4 t6
∀H12:getl (r (Bind b) i1) c0 (CHead d0 (Bind Abbr) u0)
.pc3 (CHead c0 (Bind b) t) t4 t6
assume f: F
suppose H12: getl (r (Flat f) i1) c0 (CHead d0 (Bind Abbr) u0)
consider H11
we proved subst0 (S i1) u0 t5 t6
that is equivalent to subst0 (r (Flat f) i1) u0 t5 t6
by (pr2_delta . . . . H12 . . H6 . previous)
we proved pr2 c0 t4 t6
by (pr2_cflat . . . previous . .)
we proved pr2 (CHead c0 (Flat f) t) t4 t6
by (pc3_pr2_r . . . previous)
we proved pc3 (CHead c0 (Flat f) t) t4 t6
∀H12:getl (r (Flat f) i1) c0 (CHead d0 (Bind Abbr) u0)
.pc3 (CHead c0 (Flat f) t) t4 t6
by (previous . previous)
we proved pc3 (CHead c0 k t) t4 t6
∀H10:getl (S i1) (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)
.∀H11:(subst0 (S i1) u0 t5 t6).(pc3 (CHead c0 k t) t4 t6)
by (previous . H9 H7)
we proved pc3 (CHead c0 k t) t4 t6
∀H8:(eq C c1 (CHead c0 k t1)).(pc3 (CHead c0 k t) t4 t6)
we proved (eq C y (CHead c0 k t1))→(pc3 (CHead c0 k t) t0 t3)
we proved ∀y:C.(pr2 y t0 t3)→(eq C y (CHead c0 k t1))→(pc3 (CHead c0 k t) t0 t3)
by (insert_eq . . . . previous H3)
we proved pc3 (CHead c0 k t) t0 t3
∀t0:T.∀t3:T.∀k:K.∀H3:(pr2 (CHead c0 k t1) t0 t3).(pc3 (CHead c0 k t) t0 t3)
we proved ∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)
we proved ∀c:C.∀u1:T.∀u2:T.(pr2 c u2 u1)→∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pc3 (CHead c k u1) t1 t2)