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