DEFINITION pr2_head_2()
TYPE =
∀c:C.∀u:T.∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u) t1 t2)→(pr2 c (THead k u t1) (THead k u t2))
BODY =
assume c: C
assume u: T
assume t1: T
assume t2: T
assume k: K
suppose H: pr2 (CHead c k u) t1 t2
assume y: C
suppose H0: pr2 y t1 t2
we proceed by induction on H0 to prove (eq C y (CHead c k u))→(pr2 c (THead k u t1) (THead k u t2))
case pr2_free : c0:C t3:T t4:T H1:pr0 t3 t4 ⇒
the thesis becomes (eq C c0 (CHead c k u))→(pr2 c (THead k u t3) (THead k u t4))
suppose : eq C c0 (CHead c k u)
by (pr0_refl .)
we proved pr0 u u
by (pr0_comp . . previous . . H1 .)
we proved pr0 (THead k u t3) (THead k u t4)
by (pr2_free . . . previous)
we proved pr2 c (THead k u t3) (THead k u t4)
(eq C c0 (CHead c k u))→(pr2 c (THead k u t3) (THead k u t4))
case pr2_delta ⇒
we need to prove
∀c0:C
.∀d:C
.∀u0:T
.∀i:nat
.getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c k u))→(pr2 c (THead k u t3) (THead k u t))
we proceed by induction on k to prove
∀c0:C
.∀d:C
.∀u0:T
.∀i:nat
.getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c k u))→(pr2 c (THead k u t3) (THead k u t))
case Bind : b:B ⇒
the thesis becomes
∀c0:C
.∀d:C
.∀u0:T
.∀i:nat
.getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Bind b) u)
→pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
assume c0: C
assume d: C
assume u0: T
assume i: nat
we proceed by induction on i to prove
getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Bind b) u)
→pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
case O : ⇒
the thesis becomes
getl O c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 O u0 t4 t
→(eq C c0 (CHead c (Bind b) u)
→pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
suppose H1: getl O c0 (CHead d (Bind Abbr) u0)
assume t3: T
assume t4: T
suppose H2: pr0 t3 t4
assume t: T
suppose H3: subst0 O u0 t4 t
suppose H4: eq C c0 (CHead c (Bind b) u)
(H5)
we proceed by induction on H4 to prove getl O (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl O (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
end of H5
(H6)
by (getl_gen_O . . H5)
we proved clear (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d (Bind Abbr) u0) (CHead c (Bind b) u)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead c (Bind b) u OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abbr) u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c1 ⇒c1 (CHead c (Bind b) u)
end of H6
(h1)
(H7)
by (getl_gen_O . . H5)
we proved clear (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d (Bind Abbr) u0) (CHead c (Bind b) u)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c (Bind b) u 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) u0
λ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) u
end of H7
(h1)
(H8)
by (getl_gen_O . . H5)
we proved clear (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
by (clear_gen_bind . . . . previous)
we proved eq C (CHead d (Bind Abbr) u0) (CHead c (Bind b) u)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead c (Bind b) u OF CSort ⇒u0 | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t0⇒t0 (CHead d (Bind Abbr) u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t0⇒t0 (CHead c (Bind b) u)
end of H8
suppose H9: eq B Abbr b
suppose : eq C d c
(H11)
consider H8
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u0 OF CSort ⇒u0 | CHead t0⇒t0
<λ:C.T> CASE CHead c (Bind b) u OF CSort ⇒u0 | CHead t0⇒t0
that is equivalent to eq T u0 u
we proceed by induction on the previous result to prove subst0 O u t4 t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 O u t4 t
end of H11
we proceed by induction on H9 to prove pr2 c (THead (Bind b) u t3) (THead (Bind b) u t)
case refl_equal : ⇒
the thesis becomes pr2 c (THead (Bind Abbr) u t3) (THead (Bind Abbr) u t)
by (pr0_refl .)
we proved pr0 u u
by (pr0_delta . . previous . . H2 . H11)
we proved pr0 (THead (Bind Abbr) u t3) (THead (Bind Abbr) u t)
by (pr2_free . . . previous)
pr2 c (THead (Bind Abbr) u t3) (THead (Bind Abbr) u t)
we proved pr2 c (THead (Bind b) u t3) (THead (Bind b) u t)
eq B Abbr b
→(eq C d c)→(pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
end of h1
(h2)
consider H7
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u0 OF
CSort ⇒Abbr
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c (Bind b) u 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)→(pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead c (Bind b) u OF CSort ⇒d | CHead c1 ⇒c1
eq C d c
end of h2
by (h1 h2)
we proved pr2 c (THead (Bind b) u t3) (THead (Bind b) u t)
getl O c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 O u0 t4 t
→(eq C c0 (CHead c (Bind b) u)
→pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
case S : n:nat ⇒
the thesis becomes
∀H2:getl (S n) c0 (CHead d (Bind Abbr) u0)
.∀t3:T
.∀t4:T
.∀H3:pr0 t3 t4
.∀t:T
.∀H4:subst0 (S n) u0 t4 t
.∀H5:eq C c0 (CHead c (Bind b) u)
.pr2 c (THead (Bind b) u t3) (THead (Bind b) u t)
(H1) by induction hypothesis we know
getl n c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 n u0 t4 t
→(eq C c0 (CHead c (Bind b) u)
→pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
suppose H2: getl (S n) c0 (CHead d (Bind Abbr) u0)
assume t3: T
assume t4: T
suppose H3: pr0 t3 t4
assume t: T
suppose H4: subst0 (S n) u0 t4 t
suppose H5: eq C c0 (CHead c (Bind b) u)
(H6)
we proceed by induction on H5 to prove getl (S n) (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
getl (S n) (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
end of H6
(h1)
by (getl_gen_S . . . . . H6)
getl (r (Bind b) n) c (CHead d (Bind Abbr) u0)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 u u
by (pr0_comp . . previous . . H3 .)
pr0 (THead (Bind b) u t3) (THead (Bind b) u t4)
end of h2
(h3)
consider H4
we proved subst0 (S n) u0 t4 t
that is equivalent to subst0 (s (Bind b) (r (Bind b) n)) u0 t4 t
by (subst0_snd . . . . . previous .)
subst0 (r (Bind b) n) u0 (THead (Bind b) u t4) (THead (Bind b) u t)
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
we proved pr2 c (THead (Bind b) u t3) (THead (Bind b) u t)
∀H2:getl (S n) c0 (CHead d (Bind Abbr) u0)
.∀t3:T
.∀t4:T
.∀H3:pr0 t3 t4
.∀t:T
.∀H4:subst0 (S n) u0 t4 t
.∀H5:eq C c0 (CHead c (Bind b) u)
.pr2 c (THead (Bind b) u t3) (THead (Bind b) u t)
we proved
getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Bind b) u)
→pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
∀c0:C
.∀d:C
.∀u0:T
.∀i:nat
.getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Bind b) u)
→pr2 c (THead (Bind b) u t3) (THead (Bind b) u t))
case Flat : f:F ⇒
the thesis becomes
∀c0:C
.∀d:C
.∀u0:T
.∀i:nat
.getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Flat f) u)
→pr2 c (THead (Flat f) u t3) (THead (Flat f) u t))
assume c0: C
assume d: C
assume u0: T
assume i: nat
we proceed by induction on i to prove
getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Flat f) u)
→pr2 c (THead (Flat f) u t3) (THead (Flat f) u t))
case O : ⇒
the thesis becomes
getl O c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 O u0 t4 t
→(eq C c0 (CHead c (Flat f) u)
→pr2 c (THead (Flat f) u t3) (THead (Flat f) u t))
suppose H1: getl O c0 (CHead d (Bind Abbr) u0)
assume t3: T
assume t4: T
suppose H2: pr0 t3 t4
assume t: T
suppose H3: subst0 O u0 t4 t
suppose H4: eq C c0 (CHead c (Flat f) u)
(H5)
we proceed by induction on H4 to prove getl O (CHead c (Flat f) u) (CHead d (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl O (CHead c (Flat f) u) (CHead d (Bind Abbr) u0)
end of H5
(h1)
(h1)
by (drop_refl .)
drop O O c c
end of h1
(h2)
by (getl_gen_O . . H5)
we proved clear (CHead c (Flat f) u) (CHead d (Bind Abbr) u0)
by (clear_gen_flat . . . . previous)
clear c (CHead d (Bind Abbr) u0)
end of h2
by (getl_intro . . . . h1 h2)
getl O c (CHead d (Bind Abbr) u0)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 u u
by (pr0_comp . . previous . . H2 .)
pr0 (THead (Flat f) u t3) (THead (Flat f) u t4)
end of h2
(h3)
consider H3
we proved subst0 O u0 t4 t
that is equivalent to subst0 (s (Flat f) O) u0 t4 t
by (subst0_snd . . . . . previous .)
subst0 O u0 (THead (Flat f) u t4) (THead (Flat f) u t)
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
we proved pr2 c (THead (Flat f) u t3) (THead (Flat f) u t)
getl O c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 O u0 t4 t
→(eq C c0 (CHead c (Flat f) u)
→pr2 c (THead (Flat f) u t3) (THead (Flat f) u t))
case S : n:nat ⇒
the thesis becomes
∀H2:getl (S n) c0 (CHead d (Bind Abbr) u0)
.∀t3:T
.∀t4:T
.∀H3:pr0 t3 t4
.∀t:T
.∀H4:subst0 (S n) u0 t4 t
.∀H5:eq C c0 (CHead c (Flat f) u)
.pr2 c (THead (Flat f) u t3) (THead (Flat f) u t)
(H1) by induction hypothesis we know
getl n c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 n u0 t4 t
→(eq C c0 (CHead c (Flat f) u)
→pr2 c (THead (Flat f) u t3) (THead (Flat f) u t))
suppose H2: getl (S n) c0 (CHead d (Bind Abbr) u0)
assume t3: T
assume t4: T
suppose H3: pr0 t3 t4
assume t: T
suppose H4: subst0 (S n) u0 t4 t
suppose H5: eq C c0 (CHead c (Flat f) u)
(H6)
we proceed by induction on H5 to prove getl (S n) (CHead c (Flat f) u) (CHead d (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
getl (S n) (CHead c (Flat f) u) (CHead d (Bind Abbr) u0)
end of H6
(h1)
by (getl_gen_S . . . . . H6)
getl (r (Flat f) n) c (CHead d (Bind Abbr) u0)
end of h1
(h2)
by (pr0_refl .)
we proved pr0 u u
by (pr0_comp . . previous . . H3 .)
pr0 (THead (Flat f) u t3) (THead (Flat f) u t4)
end of h2
(h3)
consider H4
we proved subst0 (S n) u0 t4 t
that is equivalent to subst0 (s (Flat f) (r (Flat f) n)) u0 t4 t
by (subst0_snd . . . . . previous .)
subst0 (r (Flat f) n) u0 (THead (Flat f) u t4) (THead (Flat f) u t)
end of h3
by (pr2_delta . . . . h1 . . h2 . h3)
we proved pr2 c (THead (Flat f) u t3) (THead (Flat f) u t)
∀H2:getl (S n) c0 (CHead d (Bind Abbr) u0)
.∀t3:T
.∀t4:T
.∀H3:pr0 t3 t4
.∀t:T
.∀H4:subst0 (S n) u0 t4 t
.∀H5:eq C c0 (CHead c (Flat f) u)
.pr2 c (THead (Flat f) u t3) (THead (Flat f) u t)
we proved
getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Flat f) u)
→pr2 c (THead (Flat f) u t3) (THead (Flat f) u t))
∀c0:C
.∀d:C
.∀u0:T
.∀i:nat
.getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c (Flat f) u)
→pr2 c (THead (Flat f) u t3) (THead (Flat f) u t))
∀c0:C
.∀d:C
.∀u0:T
.∀i:nat
.getl i c0 (CHead d (Bind Abbr) u0)
→∀t3:T
.∀t4:T
.pr0 t3 t4
→∀t:T
.subst0 i u0 t4 t
→(eq C c0 (CHead c k u))→(pr2 c (THead k u t3) (THead k u t))
we proved (eq C y (CHead c k u))→(pr2 c (THead k u t1) (THead k u t2))
we proved
∀y:C
.pr2 y t1 t2
→(eq C y (CHead c k u))→(pr2 c (THead k u t1) (THead k u t2))
by (insert_eq . . . . previous H)
we proved pr2 c (THead k u t1) (THead k u t2)
we proved ∀c:C.∀u:T.∀t1:T.∀t2:T.∀k:K.(pr2 (CHead c k u) t1 t2)→(pr2 c (THead k u t1) (THead k u t2))