DEFINITION pr2_subst1()
TYPE =
∀c:C
.∀e:C
.∀v:T
.∀i:nat
.getl i c (CHead e (Bind Abbr) v)
→∀t1:T.∀t2:T.(pr2 c t1 t2)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t2 w2)
BODY =
assume c: C
assume e: C
assume v: T
assume i: nat
suppose H: getl i c (CHead e (Bind Abbr) v)
assume t1: T
assume t2: T
suppose H0: pr2 c t1 t2
assume y: C
suppose H1: pr2 y t1 t2
we proceed by induction on H1 to prove (eq C y c)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr2 y w1 w2 λw2:T.subst1 i v t2 w2)
case pr2_free : c0:C t3:T t4:T H2:pr0 t3 t4 ⇒
the thesis becomes ∀H3:(eq C c0 c).∀w1:T.∀H4:(subst1 i v t3 w1).(ex2 T λw2:T.pr2 c0 w1 w2 λw2:T.subst1 i v t4 w2)
suppose H3: eq C c0 c
assume w1: T
suppose H4: subst1 i v t3 w1
by (pr0_refl .)
we proved pr0 v v
by (pr0_subst1 . . H2 . . . H4 . previous)
we proved ex2 T λw2:T.pr0 w1 w2 λw2:T.subst1 i v t4 w2
we proceed by induction on the previous result to prove ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t4 w2
case ex_intro2 : x:T H5:pr0 w1 x H6:subst1 i v t4 x ⇒
the thesis becomes ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t4 w2
by (pr2_free . . . H5)
we proved pr2 c w1 x
by (ex_intro2 . . . . previous H6)
ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t4 w2
we proved ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t4 w2
by (eq_ind_r . . . previous . H3)
we proved ex2 T λw2:T.pr2 c0 w1 w2 λw2:T.subst1 i v t4 w2
∀H3:(eq C c0 c).∀w1:T.∀H4:(subst1 i v t3 w1).(ex2 T λw2:T.pr2 c0 w1 w2 λw2:T.subst1 i v t4 w2)
case pr2_delta : c0:C d:C u:T i0:nat H2:getl i0 c0 (CHead d (Bind Abbr) u) t3:T t4:T H3:pr0 t3 t4 t:T H4:subst0 i0 u t4 t ⇒
the thesis becomes ∀H5:(eq C c0 c).∀w1:T.∀H6:(subst1 i v t3 w1).(ex2 T λw2:T.pr2 c0 w1 w2 λw2:T.subst1 i v t w2)
suppose H5: eq C c0 c
assume w1: T
suppose H6: subst1 i v t3 w1
(H7)
we proceed by induction on H5 to prove getl i0 c (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
getl i0 c (CHead d (Bind Abbr) u)
end of H7
by (pr0_refl .)
we proved pr0 v v
by (pr0_subst1 . . H3 . . . H6 . previous)
we proved ex2 T λw2:T.pr0 w1 w2 λw2:T.subst1 i v t4 w2
we proceed by induction on the previous result to prove ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
case ex_intro2 : x:T H8:pr0 w1 x H9:subst1 i v t4 x ⇒
the thesis becomes ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
(h1)
suppose H10: not (eq nat i i0)
(h1)
by (subst1_single . . . . H4)
subst1 i0 u t4 t
end of h1
(h2)
by (sym_not_eq . . . H10)
not (eq nat i0 i)
end of h2
by (subst1_confluence_neq . . . . h1 . . . H9 h2)
we proved ex2 T λt:T.subst1 i v t t λt:T.subst1 i0 u x t
we proceed by induction on the previous result to prove ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
case ex_intro2 : x0:T H11:subst1 i v t x0 H12:subst1 i0 u x x0 ⇒
the thesis becomes ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
by (pr2_delta1 . . . . H7 . . H8 . H12)
we proved pr2 c w1 x0
by (ex_intro2 . . . . previous H11)
ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
we proved ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
(not (eq nat i i0))→(ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2)
end of h1
(h2)
suppose H10: eq nat i i0
(H11)
by (eq_ind_r . . . H4 . H10)
subst0 i u t4 t
end of H11
(H12)
by (eq_ind_r . . . H7 . H10)
getl i c (CHead d (Bind Abbr) u)
end of H12
(H13)
by (getl_mono . . . H . H12)
we proved eq C (CHead e (Bind Abbr) v) (CHead d (Bind Abbr) u)
we proceed by induction on the previous result to prove getl i c (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H
getl i c (CHead d (Bind Abbr) u)
end of H13
(H14)
by (getl_mono . . . H . H12)
we proved eq C (CHead e (Bind Abbr) v) (CHead d (Bind Abbr) u)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead e (Bind Abbr) v OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒e | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead e (Bind Abbr) v)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead d (Bind Abbr) u)
end of H14
(h1)
(H15)
by (getl_mono . . . H . H12)
we proved eq C (CHead e (Bind Abbr) v) (CHead d (Bind Abbr) u)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead e (Bind Abbr) v OF CSort ⇒v | CHead t0⇒t0
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒v | CHead t0⇒t0
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒v | CHead t0⇒t0 (CHead e (Bind Abbr) v)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒v | CHead t0⇒t0 (CHead d (Bind Abbr) u)
end of H15
suppose H16: eq C e d
(H17)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead e (Bind Abbr) v OF CSort ⇒v | CHead t0⇒t0
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒v | CHead t0⇒t0
that is equivalent to eq T v u
by (eq_ind_r . . . H13 . previous)
getl i c (CHead d (Bind Abbr) v)
end of H17
(H18)
consider H15
we proved
eq
T
<λ:C.T> CASE CHead e (Bind Abbr) v OF CSort ⇒v | CHead t0⇒t0
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒v | CHead t0⇒t0
that is equivalent to eq T v u
by (eq_ind_r . . . H11 . previous)
subst0 i v t4 t
end of H18
(H19)
by (eq_ind_r . . . H17 . H16)
getl i c (CHead e (Bind Abbr) v)
end of H19
by (subst1_single . . . . H18)
we proved subst1 i v t4 t
by (subst1_confluence_eq . . . . previous . H9)
we proved ex2 T λt:T.subst1 i v t t λt:T.subst1 i v x t
we proceed by induction on the previous result to prove ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
case ex_intro2 : x0:T H20:subst1 i v t x0 H21:subst1 i v x x0 ⇒
the thesis becomes ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
by (pr2_delta1 . . . . H19 . . H8 . H21)
we proved pr2 c w1 x0
by (ex_intro2 . . . . previous H20)
ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
we proved ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
(eq C e d)→(ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2)
end of h1
(h2)
consider H14
we proved
eq
C
<λ:C.C> CASE CHead e (Bind Abbr) v OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒e | CHead c1 ⇒c1
eq C e d
end of h2
by (h1 h2)
we proved ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
(eq nat i i0)→(ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2)
end of h2
by (neq_eq_e . . . h1 h2)
ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
we proved ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t w2
by (eq_ind_r . . . previous . H5)
we proved ex2 T λw2:T.pr2 c0 w1 w2 λw2:T.subst1 i v t w2
∀H5:(eq C c0 c).∀w1:T.∀H6:(subst1 i v t3 w1).(ex2 T λw2:T.pr2 c0 w1 w2 λw2:T.subst1 i v t w2)
we proved (eq C y c)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr2 y w1 w2 λw2:T.subst1 i v t2 w2)
we proved ∀y:C.(pr2 y t1 t2)→(eq C y c)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr2 y w1 w2 λw2:T.subst1 i v t2 w2)
by (insert_eq . . . . previous H0)
we proved ∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t2 w2)
we proved
∀c:C
.∀e:C
.∀v:T
.∀i:nat
.getl i c (CHead e (Bind Abbr) v)
→∀t1:T.∀t2:T.(pr2 c t1 t2)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t2 w2)