DEFINITION sn3_appl_abbr()
TYPE =
∀c:C
.∀d:C
.∀w:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) w)
→∀v:T
.sn3 c (THead (Flat Appl) v (lift (S i) O w))
→sn3 c (THead (Flat Appl) v (TLRef i))
BODY =
assume c: C
assume d: C
assume w: T
assume i: nat
suppose H: getl i c (CHead d (Bind Abbr) w)
assume v: T
suppose H0: sn3 c (THead (Flat Appl) v (lift (S i) O w))
assume y: T
suppose H1: sn3 c y
we proceed by induction on H1 to prove
∀x:T
.eq T y (THead (Flat Appl) x (lift (S i) O w))
→sn3 c (THead (Flat Appl) x (TLRef i))
case sn3_sing : t1:T H2:∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
the thesis becomes
∀x:T
.∀H4:eq T t1 (THead (Flat Appl) x (lift (S i) O w))
.sn3 c (THead (Flat Appl) x (TLRef i))
(H3) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c t1 t2
→∀x:T
.eq T t2 (THead (Flat Appl) x (lift (S i) O w))
→sn3 c (THead (Flat Appl) x (TLRef i)))
assume x: T
suppose H4: eq T t1 (THead (Flat Appl) x (lift (S i) O w))
(H5)
we proceed by induction on H4 to prove
∀t2:T
.(eq T (THead (Flat Appl) x (lift (S i) O w)) t2)→∀P:Prop.P
→(pr3 c (THead (Flat Appl) x (lift (S i) O w)) t2
→∀x0:T
.eq T t2 (THead (Flat Appl) x0 (lift (S i) O w))
→sn3 c (THead (Flat Appl) x0 (TLRef i)))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀t2:T
.(eq T (THead (Flat Appl) x (lift (S i) O w)) t2)→∀P:Prop.P
→(pr3 c (THead (Flat Appl) x (lift (S i) O w)) t2
→∀x0:T
.eq T t2 (THead (Flat Appl) x0 (lift (S i) O w))
→sn3 c (THead (Flat Appl) x0 (TLRef i)))
end of H5
(H6)
we proceed by induction on H4 to prove
∀t2:T
.(eq T (THead (Flat Appl) x (lift (S i) O w)) t2)→∀P:Prop.P
→(pr3 c (THead (Flat Appl) x (lift (S i) O w)) t2)→(sn3 c t2)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀t2:T
.(eq T (THead (Flat Appl) x (lift (S i) O w)) t2)→∀P:Prop.P
→(pr3 c (THead (Flat Appl) x (lift (S i) O w)) t2)→(sn3 c t2)
end of H6
assume t2: T
suppose H7: (eq T (THead (Flat Appl) x (TLRef i)) t2)→∀P:Prop.P
suppose H8: pr2 c (THead (Flat Appl) x (TLRef i)) t2
(H9)
by (pr2_gen_appl . . . . H8)
or3
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr2 c x u2 λ:T.λt2:T.pr2 c (TLRef i) t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr2 c x u2
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c x u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2
end of H9
we proceed by induction on H9 to prove sn3 c t2
case or3_intro0 : H10:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr2 c x u2 λ:T.λt3:T.pr2 c (TLRef i) t3 ⇒
the thesis becomes sn3 c t2
we proceed by induction on H10 to prove sn3 c t2
case ex3_2_intro : x0:T x1:T H11:eq T t2 (THead (Flat Appl) x0 x1) H12:pr2 c x x0 H13:pr2 c (TLRef i) x1 ⇒
the thesis becomes sn3 c t2
(H14)
we proceed by induction on H11 to prove
eq T (THead (Flat Appl) x (TLRef i)) (THead (Flat Appl) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H7
eq T (THead (Flat Appl) x (TLRef i)) (THead (Flat Appl) x0 x1)
→∀P:Prop.P
end of H14
(H15)
by (pr2_gen_lref . . . H13)
or
eq T x1 (TLRef i)
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abbr) u)
λ:C.λu:T.eq T x1 (lift (S i) O u)
end of H15
we proceed by induction on H15 to prove sn3 c (THead (Flat Appl) x0 x1)
case or_introl : H16:eq T x1 (TLRef i) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 x1)
(H17)
we proceed by induction on H16 to prove
(eq
T
THead (Flat Appl) x (TLRef i)
THead (Flat Appl) x0 (TLRef i))
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H14
(eq
T
THead (Flat Appl) x (TLRef i)
THead (Flat Appl) x0 (TLRef i))
→∀P:Prop.P
end of H17
(H_x)
by (term_dec . .)
or (eq T x x0) (eq T x x0)→∀P:Prop.P
end of H_x
(H18) consider H_x
we proceed by induction on H18 to prove sn3 c (THead (Flat Appl) x0 (TLRef i))
case or_introl : H19:eq T x x0 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (TLRef i))
(H20)
by (eq_ind_r . . . H17 . H19)
(eq
T
THead (Flat Appl) x (TLRef i)
THead (Flat Appl) x (TLRef i))
→∀P:Prop.P
end of H20
we proceed by induction on H19 to prove sn3 c (THead (Flat Appl) x0 (TLRef i))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (TLRef i))
by (refl_equal . .)
we proved
eq
T
THead (Flat Appl) x (TLRef i)
THead (Flat Appl) x (TLRef i)
by (H20 previous .)
sn3 c (THead (Flat Appl) x (TLRef i))
sn3 c (THead (Flat Appl) x0 (TLRef i))
case or_intror : H19:(eq T x x0)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (TLRef i))
(h1)
suppose H20:
eq
T
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w)
assume P: Prop
(H21)
by (f_equal . . . . . H20)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) x (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x0 (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t ⇒t
THead (Flat Appl) x (lift (S i) O w)
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t ⇒t
THead (Flat Appl) x0 (lift (S i) O w)
end of H21
(H22)
consider H21
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) x (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x0 (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
that is equivalent to eq T x x0
by (eq_ind_r . . . H19 . previous)
(eq T x x)→∀P0:Prop.P0
end of H22
by (refl_equal . .)
we proved eq T x x
by (H22 previous .)
we proved P
(eq
T
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w))
→∀P:Prop.P
end of h1
(h2)
by (pr2_head_1 . . . H12 . .)
we proved
pr2
c
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w)
by (pr3_pr2 . . . previous)
pr3
c
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w)
end of h2
(h3)
by (refl_equal . .)
eq
T
THead (Flat Appl) x0 (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w)
end of h3
by (H5 . h1 h2 . h3)
sn3 c (THead (Flat Appl) x0 (TLRef i))
we proved sn3 c (THead (Flat Appl) x0 (TLRef i))
by (eq_ind_r . . . previous . H16)
sn3 c (THead (Flat Appl) x0 x1)
case or_intror : H16:ex2_2 C T λd0:C.λu:T.getl i c (CHead d0 (Bind Abbr) u) λ:C.λu:T.eq T x1 (lift (S i) O u) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 x1)
we proceed by induction on H16 to prove sn3 c (THead (Flat Appl) x0 x1)
case ex2_2_intro : x2:C x3:T H17:getl i c (CHead x2 (Bind Abbr) x3) H18:eq T x1 (lift (S i) O x3) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 x1)
(H20)
by (getl_mono . . . H . H17)
we proved eq C (CHead d (Bind Abbr) w) (CHead x2 (Bind Abbr) x3)
we proceed by induction on the previous result to prove getl i c (CHead x2 (Bind Abbr) x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H
getl i c (CHead x2 (Bind Abbr) x3)
end of H20
(H21)
by (getl_mono . . . H . H17)
we proved eq C (CHead d (Bind Abbr) w) (CHead x2 (Bind Abbr) x3)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) w OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x2 (Bind Abbr) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) w)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead x2 (Bind Abbr) x3)
end of H21
(h1)
(H22)
by (getl_mono . . . H . H17)
we proved eq C (CHead d (Bind Abbr) w) (CHead x2 (Bind Abbr) x3)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead x2 (Bind Abbr) x3 OF CSort ⇒w | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒w | CHead t⇒t (CHead d (Bind Abbr) w)
λe:C.<λ:C.T> CASE e OF CSort ⇒w | CHead t⇒t (CHead x2 (Bind Abbr) x3)
end of H22
suppose H23: eq C d x2
(H24)
consider H22
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead x2 (Bind Abbr) x3 OF CSort ⇒w | CHead t⇒t
that is equivalent to eq T w x3
by (eq_ind_r . . . H20 . previous)
getl i c (CHead x2 (Bind Abbr) w)
end of H24
consider H22
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) w OF CSort ⇒w | CHead t⇒t
<λ:C.T> CASE CHead x2 (Bind Abbr) x3 OF CSort ⇒w | CHead t⇒t
that is equivalent to eq T w x3
we proceed by induction on the previous result to prove sn3 c (THead (Flat Appl) x0 (lift (S i) O x3))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
(H_x)
by (term_dec . .)
or (eq T x x0) (eq T x x0)→∀P:Prop.P
end of H_x
(H26) consider H_x
we proceed by induction on H26 to prove sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
case or_introl : H27:eq T x x0 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
we proceed by induction on H27 to prove sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (lift (S i) O w))
by (sn3_sing . . H6)
sn3 c (THead (Flat Appl) x (lift (S i) O w))
sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
case or_intror : H27:(eq T x x0)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
(h1)
suppose H28:
eq
T
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w)
assume P: Prop
(H29)
by (f_equal . . . . . H28)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) x (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x0 (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t ⇒t
THead (Flat Appl) x (lift (S i) O w)
λe:T.<λ:T.T> CASE e OF TSort ⇒x | TLRef ⇒x | THead t ⇒t
THead (Flat Appl) x0 (lift (S i) O w)
end of H29
(H30)
consider H29
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) x (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
<λ:T.T>
CASE THead (Flat Appl) x0 (lift (S i) O w) OF
TSort ⇒x
| TLRef ⇒x
| THead t ⇒t
that is equivalent to eq T x x0
by (eq_ind_r . . . H27 . previous)
(eq T x x)→∀P0:Prop.P0
end of H30
by (refl_equal . .)
we proved eq T x x
by (H30 previous .)
we proved P
(eq
T
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w))
→∀P:Prop.P
end of h1
(h2)
by (pr2_head_1 . . . H12 . .)
we proved
pr2
c
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w)
by (pr3_pr2 . . . previous)
pr3
c
THead (Flat Appl) x (lift (S i) O w)
THead (Flat Appl) x0 (lift (S i) O w)
end of h2
by (H6 . h1 h2)
sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
sn3 c (THead (Flat Appl) x0 (lift (S i) O w))
we proved sn3 c (THead (Flat Appl) x0 (lift (S i) O x3))
(eq C d x2)→(sn3 c (THead (Flat Appl) x0 (lift (S i) O x3)))
end of h1
(h2)
consider H21
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) w OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead x2 (Bind Abbr) x3 OF CSort ⇒d | CHead c0 ⇒c0
eq C d x2
end of h2
by (h1 h2)
we proved sn3 c (THead (Flat Appl) x0 (lift (S i) O x3))
by (eq_ind_r . . . previous . H18)
sn3 c (THead (Flat Appl) x0 x1)
sn3 c (THead (Flat Appl) x0 x1)
we proved sn3 c (THead (Flat Appl) x0 x1)
by (eq_ind_r . . . previous . H11)
sn3 c t2
sn3 c t2
case or3_intro1 : H10:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3) λ:T.λ:T.λu2:T.λ:T.pr2 c x u2 λ:T.λz1:T.λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t3) ⇒
the thesis becomes sn3 c t2
we proceed by induction on H10 to prove sn3 c t2
case ex4_4_intro : x0:T x1:T x2:T x3:T H11:eq T (TLRef i) (THead (Bind Abst) x0 x1) H12:eq T t2 (THead (Bind Abbr) x2 x3) :pr2 c x x2 :∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 x3) ⇒
the thesis becomes sn3 c t2
(H16)
we proceed by induction on H11 to prove
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H16
consider H16
we proved
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove sn3 c (THead (Bind Abbr) x2 x3)
we proved sn3 c (THead (Bind Abbr) x2 x3)
by (eq_ind_r . . . previous . H12)
sn3 c t2
sn3 c t2
case or3_intro2 : H10:ex6_6 B T T T T T λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst) λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c x u2 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2 ⇒
the thesis becomes sn3 c t2
we proceed by induction on H10 to prove sn3 c t2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T :not (eq B x0 Abst) H12:eq T (TLRef i) (THead (Bind x0) x1 x2) H13:eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) :pr2 c x x4 :pr2 c x1 x5 :pr2 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes sn3 c t2
(H18)
we proceed by induction on H12 to prove
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H18
consider H18
we proved
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove sn3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
we proved sn3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
by (eq_ind_r . . . previous . H13)
sn3 c t2
sn3 c t2
we proved sn3 c t2
we proved
∀t2:T
.(eq T (THead (Flat Appl) x (TLRef i)) t2)→∀P:Prop.P
→(pr2 c (THead (Flat Appl) x (TLRef i)) t2)→(sn3 c t2)
by (sn3_pr2_intro . . previous)
we proved sn3 c (THead (Flat Appl) x (TLRef i))
∀x:T
.∀H4:eq T t1 (THead (Flat Appl) x (lift (S i) O w))
.sn3 c (THead (Flat Appl) x (TLRef i))
we proved
∀x:T
.eq T y (THead (Flat Appl) x (lift (S i) O w))
→sn3 c (THead (Flat Appl) x (TLRef i))
by (unintro . . . previous)
we proved
eq T y (THead (Flat Appl) v (lift (S i) O w))
→sn3 c (THead (Flat Appl) v (TLRef i))
we proved
∀y:T
.sn3 c y
→(eq T y (THead (Flat Appl) v (lift (S i) O w))
→sn3 c (THead (Flat Appl) v (TLRef i)))
by (insert_eq . . . . previous H0)
we proved sn3 c (THead (Flat Appl) v (TLRef i))
we proved
∀c:C
.∀d:C
.∀w:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) w)
→∀v:T
.sn3 c (THead (Flat Appl) v (lift (S i) O w))
→sn3 c (THead (Flat Appl) v (TLRef i))