DEFINITION pr2_gen_cbind()
TYPE =
∀b:B
.∀c:C
.∀v:T
.∀t1:T
.∀t2:T
.pr2 (CHead c (Bind b) v) t1 t2
→pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2)
BODY =
assume b: B
assume c: C
assume v: T
assume t1: T
assume t2: T
suppose H: pr2 (CHead c (Bind b) v) t1 t2
assume y: C
suppose H0: pr2 y t1 t2
we proceed by induction on H0 to prove
eq C y (CHead c (Bind b) v)
→pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2)
case pr2_free : c0:C t3:T t4:T H1:pr0 t3 t4 ⇒
the thesis becomes
eq C c0 (CHead c (Bind b) v)
→pr2 c (THead (Bind b) v t3) (THead (Bind b) v t4)
suppose : eq C c0 (CHead c (Bind b) v)
by (pr0_refl .)
we proved pr0 v v
by (pr0_comp . . previous . . H1 .)
we proved pr0 (THead (Bind b) v t3) (THead (Bind b) v t4)
by (pr2_free . . . previous)
we proved pr2 c (THead (Bind b) v t3) (THead (Bind b) v t4)
eq C c0 (CHead c (Bind b) v)
→pr2 c (THead (Bind b) v t3) (THead (Bind b) v t4)
case pr2_delta : c0:C d:C u:T i:nat H1:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H2:pr0 t3 t4 t:T H3:subst0 i u t4 t ⇒
the thesis becomes
∀H4:eq C c0 (CHead c (Bind b) v)
.pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
suppose H4: eq C c0 (CHead c (Bind b) v)
(H5)
we proceed by induction on H4 to prove getl i (CHead c (Bind b) v) (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl i (CHead c (Bind b) v) (CHead d (Bind Abbr) u)
end of H5
(H_x)
by (getl_gen_bind . . . . . H5)
or
land
eq nat i O
eq C (CHead d (Bind Abbr) u) (CHead c (Bind b) v)
ex2
nat
λj:nat.eq nat i (S j)
λj:nat.getl j c (CHead d (Bind Abbr) u)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
case or_introl : H7:land (eq nat i O) (eq C (CHead d (Bind Abbr) u) (CHead c (Bind b) v)) ⇒
the thesis becomes pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
we proceed by induction on H7 to prove pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
case conj : H8:eq nat i O H9:eq C (CHead d (Bind Abbr) u) (CHead c (Bind b) v) ⇒
the thesis becomes pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
(H10)
by (f_equal . . . . . H9)
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) v 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) v)
end of H10
(h1)
(H11)
by (f_equal . . . . . H9)
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c (Bind b) v OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
eq
B
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
CHead d (Bind Abbr) u
λe:C
.<λ:C.B>
CASE e OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
CHead c (Bind b) v
end of H11
(h1)
(H12)
by (f_equal . . . . . H9)
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) v 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) v)
end of H12
suppose H13: eq B Abbr b
suppose : eq C d c
(H15)
we proceed by induction on H8 to prove subst0 O u t4 t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 O u t4 t
end of H15
(H16)
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) v OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u v
we proceed by induction on the previous result to prove subst0 O v t4 t
case refl_equal : ⇒
the thesis becomes the hypothesis H15
subst0 O v t4 t
end of H16
we proceed by induction on H13 to prove pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
case refl_equal : ⇒
the thesis becomes pr2 c (THead (Bind Abbr) v t3) (THead (Bind Abbr) v t)
by (pr0_refl .)
we proved pr0 v v
by (pr0_delta . . previous . . H2 . H16)
we proved pr0 (THead (Bind Abbr) v t3) (THead (Bind Abbr) v t)
by (pr2_free . . . previous)
pr2 c (THead (Bind Abbr) v t3) (THead (Bind Abbr) v t)
we proved pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
eq B Abbr b
→(eq C d c)→(pr2 c (THead (Bind b) v t3) (THead (Bind b) v t))
end of h1
(h2)
consider H11
we proved
eq
B
<λ:C.B>
CASE CHead d (Bind Abbr) u OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒Abbr
<λ:C.B>
CASE CHead c (Bind b) v OF
CSort ⇒Abbr
| CHead k ⇒<λ:K.B> CASE k 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) v t3) (THead (Bind b) v 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) v OF CSort ⇒d | CHead c1 ⇒c1
eq C d c
end of h2
by (h1 h2)
pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
case or_intror : H7:ex2 nat λj:nat.eq nat i (S j) λj:nat.getl j c (CHead d (Bind Abbr) u) ⇒
the thesis becomes pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
we proceed by induction on H7 to prove pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
case ex_intro2 : x:nat H8:eq nat i (S x) H9:getl x c (CHead d (Bind Abbr) u) ⇒
the thesis becomes pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
(H10)
by (f_equal . . . . . H8)
we proved eq nat i (S x)
eq nat (λe:nat.e i) (λe:nat.e (S x))
end of H10
(H11)
we proceed by induction on H10 to prove subst0 (S x) u t4 t
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 (S x) u t4 t
end of H11
by (clear_bind . . .)
we proved clear (CHead c (Bind b) v) (CHead c (Bind b) v)
by (getl_clear_bind . . . . previous . . H9)
we proved getl (S x) (CHead c (Bind b) v) (CHead d (Bind Abbr) u)
by (pr2_delta . . . . previous . . H2 . H11)
we proved pr2 (CHead c (Bind b) v) t3 t
by (pr2_head_2 . . . . . previous)
pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
we proved pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
∀H4:eq C c0 (CHead c (Bind b) v)
.pr2 c (THead (Bind b) v t3) (THead (Bind b) v t)
we proved
eq C y (CHead c (Bind b) v)
→pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2)
we proved
∀y:C
.pr2 y t1 t2
→(eq C y (CHead c (Bind b) v)
→pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2))
by (insert_eq . . . . previous H)
we proved pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2)
we proved
∀b:B
.∀c:C
.∀v:T
.∀t1:T
.∀t2:T
.pr2 (CHead c (Bind b) v) t1 t2
→pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2)