DEFINITION pr3_pr0_pr2_t()
TYPE =
∀u1:T.∀u2:T.(pr0 u1 u2)→∀c:C.∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)
BODY =
assume u1: T
assume u2: T
suppose H: pr0 u1 u2
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))→(pr3 (CHead c k u1) t1 t2)
case pr2_free : c0:C t3:T t4:T H2:pr0 t3 t4 ⇒
the thesis becomes (eq C c0 (CHead c k u2))→(pr3 (CHead c k u1) t3 t4)
suppose : eq C c0 (CHead c k u2)
by (pr2_free . . . H2)
we proved pr2 (CHead c k u1) t3 t4
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c k u1) t3 t4
(eq C c0 (CHead c k u2))→(pr3 (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)).(pr3 (CHead c k u1) t3 t)
suppose H5: eq C c0 (CHead c k u2)
(H6)
we proceed by induction on H5 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 H6
suppose H7: getl O (CHead c k u2) (CHead d (Bind Abbr) u)
suppose H8: subst0 O u t4 t
assume b: B
suppose H9: getl O (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
(H10)
by (getl_gen_O . . H9)
we proved clear (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
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 H10
(h1)
(H11)
by (getl_gen_O . . H9)
we proved clear (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
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 H11
(h1)
(H12)
by (getl_gen_O . . H9)
we proved clear (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
by (clear_gen_bind . . . . previous)
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 H12
suppose H13: eq B Abbr b
suppose : eq C d c
(H15)
consider H12
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 H8
subst0 O u2 t4 t
end of H15
we proceed by induction on H13 to prove pr3 (CHead c (Bind b) u1) t3 t
case refl_equal : ⇒
the thesis becomes pr3 (CHead c (Bind Abbr) u1) t3 t
by (pr0_subst0_back . . . . H15 . 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 pr3 (CHead c (Bind Abbr) u1) t3 t
case ex_intro2 : x:T H16:subst0 O u1 t4 x H17:pr0 x t ⇒
the thesis becomes pr3 (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 . H16)
pr2 (CHead c (Bind Abbr) u1) t3 x
end of h1
(h2)
by (pr2_free . . . H17)
we proved pr2 (CHead c (Bind Abbr) u1) x t
by (pr3_pr2 . . . previous)
pr3 (CHead c (Bind Abbr) u1) x t
end of h2
by (pr3_sing . . . h1 . h2)
pr3 (CHead c (Bind Abbr) u1) t3 t
pr3 (CHead c (Bind Abbr) u1) t3 t
we proved pr3 (CHead c (Bind b) u1) t3 t
(eq B Abbr b)→(eq C d c)→(pr3 (CHead c (Bind b) u1) t3 t)
end of h1
(h2)
consider H11
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)→(pr3 (CHead c (Bind b) u1) t3 t)
end of h1
(h2)
consider H10
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 pr3 (CHead c (Bind b) u1) t3 t
∀H9:getl O (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
.pr3 (CHead c (Bind b) u1) t3 t
assume f: F
suppose H9: getl O (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)
(h1)
by (drop_refl .)
drop O O c c
end of h1
(h2)
by (getl_gen_O . . H9)
we proved clear (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)
by (clear_gen_flat . . . . previous)
clear c (CHead d (Bind Abbr) u)
end of h2
by (getl_intro . . . . h1 h2)
we proved getl O c (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H3 . H8)
we proved pr2 c t3 t
by (pr2_cflat . . . previous . .)
we proved pr2 (CHead c (Flat f) u1) t3 t
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c (Flat f) u1) t3 t
∀H9:getl O (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)
.pr3 (CHead c (Flat f) u1) t3 t
by (previous . H7)
we proved pr3 (CHead c k u1) t3 t
getl O (CHead c k u2) (CHead d (Bind Abbr) u)
→(subst0 O u t4 t)→(pr3 (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)→(pr3 (CHead c k u1) t3 t)
suppose H7: getl (S i0) (CHead c k u2) (CHead d (Bind Abbr) u)
suppose H8: subst0 (S i0) u t4 t
assume b: B
suppose H9: getl (S i0) (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
suppose :
getl i0 (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
→(subst0 i0 u t4 t)→(pr3 (CHead c (Bind b) u1) t3 t)
by (getl_gen_S . . . . . H9)
we proved getl (r (Bind b) i0) c (CHead d (Bind Abbr) u)
by (getl_head . . . . previous .)
we proved getl (S i0) (CHead c (Bind b) u1) (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H3 . H8)
we proved pr2 (CHead c (Bind b) u1) t3 t
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c (Bind b) u1) t3 t
∀H9:getl (S i0) (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
.getl i0 (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)
→(subst0 i0 u t4 t)→(pr3 (CHead c (Bind b) u1) t3 t)
→pr3 (CHead c (Bind b) u1) t3 t
assume f: F
suppose H9: getl (S i0) (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)
suppose :
getl i0 (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)
→(subst0 i0 u t4 t)→(pr3 (CHead c (Flat f) u1) t3 t)
(h1)
by (getl_gen_S . . . . . H9)
getl (r (Flat f) i0) c (CHead d (Bind Abbr) u)
end of h1
(h2)
consider H8
we proved subst0 (S i0) u t4 t
subst0 (r (Flat f) i0) u t4 t
end of h2
by (pr2_delta . . . . h1 . . H3 . h2)
we proved pr2 c t3 t
by (pr2_cflat . . . previous . .)
we proved pr2 (CHead c (Flat f) u1) t3 t
by (pr3_pr2 . . . previous)
we proved pr3 (CHead c (Flat f) u1) t3 t
∀H9:getl (S i0) (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)
.getl i0 (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)
→(subst0 i0 u t4 t)→(pr3 (CHead c (Flat f) u1) t3 t)
→pr3 (CHead c (Flat f) u1) t3 t
by (previous . H7 IHi)
we proved pr3 (CHead c k u1) t3 t
∀H7:getl (S i0) (CHead c k u2) (CHead d (Bind Abbr) u)
.∀H8:(subst0 (S i0) u t4 t).(pr3 (CHead c k u1) t3 t)
by (previous . H6 H4)
we proved pr3 (CHead c k u1) t3 t
∀H5:(eq C c0 (CHead c k u2)).(pr3 (CHead c k u1) t3 t)
we proved (eq C y (CHead c k u2))→(pr3 (CHead c k u1) t1 t2)
we proved ∀y:C.(pr2 y t1 t2)→(eq C y (CHead c k u2))→(pr3 (CHead c k u1) t1 t2)
by (insert_eq . . . . previous H0)
we proved pr3 (CHead c k u1) t1 t2
we proved ∀u1:T.∀u2:T.(pr0 u1 u2)→∀c:C.∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u2) t1 t2)→(pr3 (CHead c k u1) t1 t2)