DEFINITION sn3_abbr()
TYPE =
∀c:C
.∀d:C
.∀v:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) v)
→(sn3 d v)→(sn3 c (TLRef i))
BODY =
assume c: C
assume d: C
assume v: T
assume i: nat
suppose H: getl i c (CHead d (Bind Abbr) v)
suppose H0: sn3 d v
assume t2: T
suppose H1: (eq T (TLRef i) t2)→∀P:Prop.P
suppose H2: pr2 c (TLRef i) t2
(H3)
by (pr2_gen_lref . . . H2)
or
eq T t2 (TLRef i)
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abbr) u)
λ:C.λu:T.eq T t2 (lift (S i) O u)
end of H3
we proceed by induction on H3 to prove sn3 c t2
case or_introl : H4:eq T t2 (TLRef i) ⇒
the thesis becomes sn3 c t2
(H5)
we proceed by induction on H4 to prove (eq T (TLRef i) (TLRef i))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H1
(eq T (TLRef i) (TLRef i))→∀P:Prop.P
end of H5
by (refl_equal . .)
we proved eq T (TLRef i) (TLRef i)
by (H5 previous .)
we proved sn3 c (TLRef i)
by (eq_ind_r . . . previous . H4)
sn3 c t2
case or_intror : H4:ex2_2 C T λd0:C.λu:T.getl i c (CHead d0 (Bind Abbr) u) λ:C.λu:T.eq T t2 (lift (S i) O u) ⇒
the thesis becomes sn3 c t2
we proceed by induction on H4 to prove sn3 c t2
case ex2_2_intro : x0:C x1:T H5:getl i c (CHead x0 (Bind Abbr) x1) H6:eq T t2 (lift (S i) O x1) ⇒
the thesis becomes sn3 c t2
(H8)
by (getl_mono . . . H . H5)
we proved eq C (CHead d (Bind Abbr) v) (CHead x0 (Bind Abbr) x1)
we proceed by induction on the previous result to prove getl i c (CHead x0 (Bind Abbr) x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H
getl i c (CHead x0 (Bind Abbr) x1)
end of H8
(H9)
by (getl_mono . . . H . H5)
we proved eq C (CHead d (Bind Abbr) v) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) v OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) v)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x0 (Bind Abbr) x1)
end of H9
(h1)
(H10)
by (getl_mono . . . H . H5)
we proved eq C (CHead d (Bind Abbr) v) (CHead x0 (Bind Abbr) x1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) v OF CSort ⇒v | CHead t⇒t
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒v | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒v | CHead t⇒t (CHead d (Bind Abbr) v)
λe:C.<λ:C.T> CASE e OF CSort ⇒v | CHead t⇒t (CHead x0 (Bind Abbr) x1)
end of H10
suppose H11: eq C d x0
(H12)
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) v OF CSort ⇒v | CHead t⇒t
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒v | CHead t⇒t
that is equivalent to eq T v x1
by (eq_ind_r . . . H8 . previous)
getl i c (CHead x0 (Bind Abbr) v)
end of H12
consider H10
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) v OF CSort ⇒v | CHead t⇒t
<λ:C.T> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒v | CHead t⇒t
that is equivalent to eq T v x1
we proceed by induction on the previous result to prove sn3 c (lift (S i) O x1)
case refl_equal : ⇒
the thesis becomes sn3 c (lift (S i) O v)
(H13)
by (eq_ind_r . . . H12 . H11)
getl i c (CHead d (Bind Abbr) v)
end of H13
by (getl_drop . . . . . H13)
we proved drop (S i) O c d
by (sn3_lift . . H0 . . . previous)
sn3 c (lift (S i) O v)
we proved sn3 c (lift (S i) O x1)
(eq C d x0)→(sn3 c (lift (S i) O x1))
end of h1
(h2)
consider H9
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) v OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abbr) x1 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x0
end of h2
by (h1 h2)
we proved sn3 c (lift (S i) O x1)
by (eq_ind_r . . . previous . H6)
sn3 c t2
sn3 c t2
we proved sn3 c t2
we proved ∀t2:T.((eq T (TLRef i) t2)→∀P:Prop.P)→(pr2 c (TLRef i) t2)→(sn3 c t2)
by (sn3_pr2_intro . . previous)
we proved sn3 c (TLRef i)
we proved
∀c:C
.∀d:C
.∀v:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) v)
→(sn3 d v)→(sn3 c (TLRef i))