DEFINITION sn3_appl_bind()
TYPE =
∀b:B
.not (eq B b Abst)
→∀c:C
.∀u:T
.sn3 c u
→∀t:T
.∀v:T
.sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O v) t)
→sn3 c (THead (Flat Appl) v (THead (Bind b) u t))
BODY =
assume b: B
suppose H: not (eq B b Abst)
assume c: C
assume u: T
suppose H0: sn3 c u
we proceed by induction on H0 to prove
∀t0:T
.∀v:T
.sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O v) t0)
→sn3 c (THead (Flat Appl) v (THead (Bind b) u t0))
case sn3_sing : t1:T H1:∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
the thesis becomes
∀t:T
.∀v:T
.∀H3:sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O v) t)
.sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t))
(H2) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c t1 t2
→∀t:T
.∀v:T
.sn3 (CHead c (Bind b) t2) (THead (Flat Appl) (lift (S O) O v) t)
→sn3 c (THead (Flat Appl) v (THead (Bind b) t2 t)))
assume t: T
assume v: T
suppose H3: sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O v) t)
assume y: T
suppose H4: sn3 (CHead c (Bind b) t1) y
we proceed by induction on H4 to prove
∀x:T
.∀x0:T
.eq T y (THead (Flat Appl) (lift (S O) O x) x0)
→sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))
case sn3_sing : t2:T H5:∀t3:T.((eq T t2 t3)→∀P:Prop.P)→(pr3 (CHead c (Bind b) t1) t2 t3)→(sn3 (CHead c (Bind b) t1) t3) ⇒
the thesis becomes
∀x:T
.∀x0:T
.∀H7:eq T t2 (THead (Flat Appl) (lift (S O) O x) x0)
.sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))
(H6) by induction hypothesis we know
∀t3:T
.(eq T t2 t3)→∀P:Prop.P
→(pr3 (CHead c (Bind b) t1) t2 t3
→∀x:T
.∀x0:T
.eq T t3 (THead (Flat Appl) (lift (S O) O x) x0)
→sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0)))
assume x: T
assume x0: T
suppose H7: eq T t2 (THead (Flat Appl) (lift (S O) O x) x0)
(H8)
we proceed by induction on H7 to prove
∀t3:T
.(eq T (THead (Flat Appl) (lift (S O) O x) x0) t3)→∀P:Prop.P
→(pr3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0) t3
→∀x1:T
.∀x2:T
.eq T t3 (THead (Flat Appl) (lift (S O) O x1) x2)
→sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x2)))
case refl_equal : ⇒
the thesis becomes the hypothesis H6
∀t3:T
.(eq T (THead (Flat Appl) (lift (S O) O x) x0) t3)→∀P:Prop.P
→(pr3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0) t3
→∀x1:T
.∀x2:T
.eq T t3 (THead (Flat Appl) (lift (S O) O x1) x2)
→sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x2)))
end of H8
(H9)
we proceed by induction on H7 to prove
∀t3:T
.(eq T (THead (Flat Appl) (lift (S O) O x) x0) t3)→∀P:Prop.P
→(pr3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0) t3
→sn3 (CHead c (Bind b) t1) t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
∀t3:T
.(eq T (THead (Flat Appl) (lift (S O) O x) x0) t3)→∀P:Prop.P
→(pr3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0) t3
→sn3 (CHead c (Bind b) t1) t3)
end of H9
assume t3: T
suppose H10: (eq T (THead (Flat Appl) x (THead (Bind b) t1 x0)) t3)→∀P:Prop.P
suppose H11: pr2 c (THead (Flat Appl) x (THead (Bind b) t1 x0)) t3
(H12)
by (pr2_gen_appl . . . . H11)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T t3 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr2 c x u2
λ:T.λt2:T.pr2 c (THead (Bind b) t1 x0) t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind b) t1 x0) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t3 (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 (THead (Bind b) t1 x0) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T.eq T t3 (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 H12
we proceed by induction on H12 to prove sn3 c t3
case or3_intro0 : H13:ex3_2 T T λu2:T.λt4:T.eq T t3 (THead (Flat Appl) u2 t4) λu2:T.λ:T.pr2 c x u2 λ:T.λt4:T.pr2 c (THead (Bind b) t1 x0) t4 ⇒
the thesis becomes sn3 c t3
we proceed by induction on H13 to prove sn3 c t3
case ex3_2_intro : x1:T x2:T H14:eq T t3 (THead (Flat Appl) x1 x2) H15:pr2 c x x1 H16:pr2 c (THead (Bind b) t1 x0) x2 ⇒
the thesis becomes sn3 c t3
(H17)
we proceed by induction on H14 to prove
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x1 x2)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H10
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x1 x2)
→∀P:Prop.P
end of H17
(H_x)
by (pr3_gen_bind . H . . . .)
pr3 c (THead (Bind b) t1 x0) x2
→(or
ex3_2
T
T
λu2:T.λt2:T.eq T x2 (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c t1 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) t1) x0 t2
pr3 (CHead c (Bind b) t1) x0 (lift (S O) O x2))
end of H_x
(H18)
by (pr3_pr2 . . . H16)
we proved pr3 c (THead (Bind b) t1 x0) x2
by (H_x previous)
or
ex3_2
T
T
λu2:T.λt2:T.eq T x2 (THead (Bind b) u2 t2)
λu2:T.λ:T.pr3 c t1 u2
λ:T.λt2:T.pr3 (CHead c (Bind b) t1) x0 t2
pr3 (CHead c (Bind b) t1) x0 (lift (S O) O x2)
end of H18
we proceed by induction on H18 to prove sn3 c (THead (Flat Appl) x1 x2)
case or_introl : H19:ex3_2 T T λu2:T.λt4:T.eq T x2 (THead (Bind b) u2 t4) λu2:T.λ:T.pr3 c t1 u2 λ:T.λt4:T.pr3 (CHead c (Bind b) t1) x0 t4 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
we proceed by induction on H19 to prove sn3 c (THead (Flat Appl) x1 x2)
case ex3_2_intro : x3:T x4:T H20:eq T x2 (THead (Bind b) x3 x4) H21:pr3 c t1 x3 H22:pr3 (CHead c (Bind b) t1) x0 x4 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
(H23)
we proceed by induction on H20 to prove
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x1 (THead (Bind b) x3 x4))
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H17
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x1 (THead (Bind b) x3 x4))
→∀P:Prop.P
end of H23
(H_x0)
by (term_dec . .)
or (eq T t1 x3) (eq T t1 x3)→∀P:Prop.P
end of H_x0
(H24) consider H_x0
we proceed by induction on H24 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3 x4))
case or_introl : H25:eq T t1 x3 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3 x4))
(H26)
by (eq_ind_r . . . H23 . H25)
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x1 (THead (Bind b) t1 x4))
→∀P:Prop.P
end of H26
we proceed by induction on H25 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
(H_x1)
by (term_dec . .)
or (eq T x0 x4) (eq T x0 x4)→∀P:Prop.P
end of H_x1
(H28) consider H_x1
we proceed by induction on H28 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
case or_introl : H29:eq T x0 x4 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
(H30)
by (eq_ind_r . . . H26 . H29)
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x1 (THead (Bind b) t1 x0))
→∀P:Prop.P
end of H30
we proceed by induction on H29 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
(H_x2)
by (term_dec . .)
or (eq T x x1) (eq T x x1)→∀P:Prop.P
end of H_x2
(H32) consider H_x2
we proceed by induction on H32 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
case or_introl : H33:eq T x x1 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
(H34)
by (eq_ind_r . . . H30 . H33)
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x (THead (Bind b) t1 x0))
→∀P:Prop.P
end of H34
we proceed by induction on H33 to prove sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))
by (refl_equal . .)
we proved
eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x (THead (Bind b) t1 x0)
by (H34 previous .)
sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))
sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
case or_intror : H33:(eq T x x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
(h1)
suppose H34:
eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0
assume P: Prop
(H35)
by (f_equal . . . . . H34)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x1) x0
end of H35
(H36)
consider H35
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
that is equivalent to eq T (lift (S O) O x) (lift (S O) O x1)
by (lift_inj . . . . previous)
we proved eq T x x1
by (eq_ind_r . . . H33 . previous)
(eq T x x)→∀P0:Prop.P0
end of H36
by (refl_equal . .)
we proved eq T x x
by (H36 previous .)
we proved P
(eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0)
→∀P:Prop.P
end of h1
(h2)
(h1)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) t1) c
end of h1
(h2) by (pr3_pr2 . . . H15) we proved pr3 c x x1
by (pr3_lift . . . . h1 . . h2)
pr3 (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1)
end of h1
(h2)
by (pr3_refl . .)
pr3 (CHead c (Bind b) t1) x0 x0
end of h2
by (pr3_flat . . . h1 . . h2 .)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0
end of h2
(h3)
by (refl_equal . .)
eq
T
THead (Flat Appl) (lift (S O) O x1) x0
THead (Flat Appl) (lift (S O) O x1) x0
end of h3
by (H8 . h1 h2 . . h3)
sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))
sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
case or_intror : H29:(eq T x0 x4)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
(h1)
suppose H30:
eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x4
assume P: Prop
(H31)
by (f_equal . . . . . H30)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x1) x4
end of H31
(h1)
(H32)
by (f_equal . . . . . H30)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x1) x4
end of H32
suppose H33: eq T (lift (S O) O x) (lift (S O) O x1)
(H34)
consider H32
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H29 . previous)
(eq T x0 x0)→∀P0:Prop.P0
end of H34
(H35)
consider H32
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H26 . previous)
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Flat Appl) x1 (THead (Bind b) t1 x0))
→∀P0:Prop.P0
end of H35
by (refl_equal . .)
we proved eq T x0 x0
by (H34 previous .)
we proved P
(eq T (lift (S O) O x) (lift (S O) O x1))→P
end of h1
(h2)
consider H31
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
eq T (lift (S O) O x) (lift (S O) O x1)
end of h2
by (h1 h2)
we proved P
(eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x4)
→∀P:Prop.P
end of h1
(h2)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) t1) c
end of h1
(h2) by (pr3_pr2 . . . H15) we proved pr3 c x x1
by (pr3_lift . . . . h1 . . h2)
we proved pr3 (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1)
by (pr3_flat . . . previous . . H22 .)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x4
end of h2
(h3)
by (refl_equal . .)
eq
T
THead (Flat Appl) (lift (S O) O x1) x4
THead (Flat Appl) (lift (S O) O x1) x4
end of h3
by (H8 . h1 h2 . . h3)
sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
sn3 c (THead (Flat Appl) x1 (THead (Bind b) t1 x4))
sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3 x4))
case or_intror : H25:(eq T t1 x3)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3 x4))
(H_x1)
by (term_dec . .)
or (eq T x0 x4) (eq T x0 x4)→∀P:Prop.P
end of H_x1
(H26) consider H_x1
we proceed by induction on H26 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)
case or_introl : H27:eq T x0 x4 ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)
we proceed by induction on H27 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)
case refl_equal : ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
(H_x2)
by (term_dec . .)
or (eq T x x1) (eq T x x1)→∀P:Prop.P
end of H_x2
(H29) consider H_x2
we proceed by induction on H29 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
case or_introl : H30:eq T x x1 ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
we proceed by induction on H30 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
case refl_equal : ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0)
by (sn3_sing . . H9)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
case or_intror : H30:(eq T x x1)→∀P:Prop.P ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
(h1)
suppose H31:
eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0
assume P: Prop
(H32)
by (f_equal . . . . . H31)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x1) x0
end of H32
(H33)
consider H32
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
that is equivalent to eq T (lift (S O) O x) (lift (S O) O x1)
by (lift_inj . . . . previous)
we proved eq T x x1
by (eq_ind_r . . . H30 . previous)
(eq T x x)→∀P0:Prop.P0
end of H33
by (refl_equal . .)
we proved eq T x x
by (H33 previous .)
we proved P
(eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0)
→∀P:Prop.P
end of h1
(h2)
(h1)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) t1) c
end of h1
(h2) by (pr3_pr2 . . . H15) we proved pr3 c x x1
by (pr3_lift . . . . h1 . . h2)
pr3 (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1)
end of h1
(h2)
by (pr3_refl . .)
pr3 (CHead c (Bind b) t1) x0 x0
end of h2
by (pr3_flat . . . h1 . . h2 .)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0
end of h2
by (H9 . h1 h2)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)
case or_intror : H27:(eq T x0 x4)→∀P:Prop.P ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)
(h1)
suppose H28:
eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x4
assume P: Prop
(H29)
by (f_equal . . . . . H28)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x1) x4
end of H29
(h1)
(H30)
by (f_equal . . . . . H28)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x1) x4
end of H30
suppose H31: eq T (lift (S O) O x) (lift (S O) O x1)
(H32)
consider H30
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H27 . previous)
(eq T x0 x0)→∀P0:Prop.P0
end of H32
by (refl_equal . .)
we proved eq T x0 x0
by (H32 previous .)
we proved P
(eq T (lift (S O) O x) (lift (S O) O x1))→P
end of h1
(h2)
consider H29
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x4 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx5:nat.plus x5 (S O)
O
x
| THead t0 ⇒t0
eq T (lift (S O) O x) (lift (S O) O x1)
end of h2
by (h1 h2)
we proved P
(eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x4)
→∀P:Prop.P
end of h1
(h2)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) t1) c
end of h1
(h2) by (pr3_pr2 . . . H15) we proved pr3 c x x1
by (pr3_lift . . . . h1 . . h2)
we proved pr3 (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1)
by (pr3_flat . . . previous . . H22 .)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x4
end of h2
by (H9 . h1 h2)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)
we proved sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x4)
by (sn3_cpr3_trans . . . H21 . . previous)
we proved sn3 (CHead c (Bind b) x3) (THead (Flat Appl) (lift (S O) O x1) x4)
by (H2 . H25 H21 . . previous)
sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3 x4))
we proved sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3 x4))
by (eq_ind_r . . . previous . H20)
sn3 c (THead (Flat Appl) x1 x2)
sn3 c (THead (Flat Appl) x1 x2)
case or_intror : H19:pr3 (CHead c (Bind b) t1) x0 (lift (S O) O x2) ⇒
the thesis becomes sn3 c (THead (Flat Appl) x1 x2)
(h1)
(h1)
(h1)
(H_x0)
by (term_dec . .)
or (eq T x x1) (eq T x x1)→∀P:Prop.P
end of H_x0
(H20) consider H_x0
we proceed by induction on H20 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
case or_introl : H21:eq T x x1 ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
we proceed by induction on H21 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
case refl_equal : ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0)
by (sn3_sing . . H9)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
case or_intror : H21:(eq T x x1)→∀P:Prop.P ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
(h1)
suppose H22:
eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0
assume P: Prop
(H23)
by (f_equal . . . . . H22)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| THead t0 ⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x1) x0
end of H23
(H24)
consider H23
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x1) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx3:nat.plus x3 (S O)
O
x
| THead t0 ⇒t0
that is equivalent to eq T (lift (S O) O x) (lift (S O) O x1)
by (lift_inj . . . . previous)
we proved eq T x x1
by (eq_ind_r . . . H21 . previous)
(eq T x x)→∀P0:Prop.P0
end of H24
by (refl_equal . .)
we proved eq T x x
by (H24 previous .)
we proved P
(eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0)
→∀P:Prop.P
end of h1
(h2)
(h1)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) t1) c
end of h1
(h2) by (pr3_pr2 . . . H15) we proved pr3 c x x1
by (pr3_lift . . . . h1 . . h2)
pr3 (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1)
end of h1
(h2)
by (pr3_refl . .)
pr3 (CHead c (Bind b) t1) x0 x0
end of h2
by (pr3_flat . . . h1 . . h2 .)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x1) x0
end of h2
by (H9 . h1 h2)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)
end of h1
(h2)
by (pr3_thin_dx . . . H19 . .)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x1) x0
THead (Flat Appl) (lift (S O) O x1) (lift (S O) O x2)
end of h2
by (sn3_pr3_trans . . h1 . h2)
we proved
sn3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x1) (lift (S O) O x2)
sn3
CHead c (Bind b) t1
THead
Flat Appl
lift (S O) O x1
lift (S O) (s (Flat Appl) O) x2
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S O) O (THead (Flat Appl) x1 x2)
THead
Flat Appl
lift (S O) O x1
lift (S O) (s (Flat Appl) O) x2
end of h2
by (eq_ind_r . . . h1 . h2)
sn3 (CHead c (Bind b) t1) (lift (S O) O (THead (Flat Appl) x1 x2))
end of h1
(h2)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) t1) c
end of h2
by (sn3_gen_lift . . . . h1 . h2)
sn3 c (THead (Flat Appl) x1 x2)
we proved sn3 c (THead (Flat Appl) x1 x2)
by (eq_ind_r . . . previous . H14)
sn3 c t3
sn3 c t3
case or3_intro1 : H13:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T (THead (Bind b) t1 x0) (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt4:T.eq T t3 (THead (Bind Abbr) u2 t4) λ:T.λ:T.λu2:T.λ:T.pr2 c x u2 λ:T.λz1:T.λ:T.λt4:T.∀b0:B.∀u0:T.(pr2 (CHead c (Bind b0) u0) z1 t4) ⇒
the thesis becomes sn3 c t3
we proceed by induction on H13 to prove sn3 c t3
case ex4_4_intro : x1:T x2:T x3:T x4:T H14:eq T (THead (Bind b) t1 x0) (THead (Bind Abst) x1 x2) H15:eq T t3 (THead (Bind Abbr) x3 x4) :pr2 c x x3 H17:∀b0:B.∀u0:T.(pr2 (CHead c (Bind b0) u0) x2 x4) ⇒
the thesis becomes sn3 c t3
(H18)
we proceed by induction on H15 to prove
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Bind Abbr) x3 x4)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H10
(eq
T
THead (Flat Appl) x (THead (Bind b) t1 x0)
THead (Bind Abbr) x3 x4)
→∀P:Prop.P
end of H18
(H19)
by (f_equal . . . . . H14)
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) t1 x0 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:T.B>
CASE THead (Bind Abst) x1 x2 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
THead (Bind b) t1 x0
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
THead (Bind Abst) x1 x2
end of H19
(h1)
(H20)
by (f_equal . . . . . H14)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) t1 x0 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x1 x2 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0 (THead (Bind b) t1 x0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
THead (Bind Abst) x1 x2
end of H20
(h1)
(H21)
by (f_equal . . . . . H14)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) t1 x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind Abst) x1 x2 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0 (THead (Bind b) t1 x0)
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Bind Abst) x1 x2
end of H21
suppose : eq T t1 x1
suppose H23: eq B b Abst
(H29)
we proceed by induction on H23 to prove not (eq B Abst Abst)
case refl_equal : ⇒
the thesis becomes the hypothesis H
not (eq B Abst Abst)
end of H29
(H30)
by (refl_equal . .)
we proved eq B Abst Abst
by (H29 previous)
we proved False
by cases on the previous result we prove sn3 c (THead (Bind Abbr) x3 x4)
sn3 c (THead (Bind Abbr) x3 x4)
end of H30
consider H30
we proved sn3 c (THead (Bind Abbr) x3 x4)
(eq T t1 x1)→(eq B b Abst)→(sn3 c (THead (Bind Abbr) x3 x4))
end of h1
(h2)
consider H20
we proved
eq
T
<λ:T.T> CASE THead (Bind b) t1 x0 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind Abst) x1 x2 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
eq T t1 x1
end of h2
by (h1 h2)
(eq B b Abst)→(sn3 c (THead (Bind Abbr) x3 x4))
end of h1
(h2)
consider H19
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) t1 x0 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:T.B>
CASE THead (Bind Abst) x1 x2 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq B b Abst
end of h2
by (h1 h2)
we proved sn3 c (THead (Bind Abbr) x3 x4)
by (eq_ind_r . . . previous . H15)
sn3 c t3
sn3 c t3
case or3_intro2 : H13:ex6_6 B T T T T T λb0:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b0 Abst) λb0:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (THead (Bind b) t1 x0) (THead (Bind b0) y1 z1) λb0:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.eq T t3 (THead (Bind b0) 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 λb0:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b0) y2) z1 z2 ⇒
the thesis becomes sn3 c t3
we proceed by induction on H13 to prove sn3 c t3
case ex6_6_intro : x1:B x2:T x3:T x4:T x5:T x6:T :not (eq B x1 Abst) H15:eq T (THead (Bind b) t1 x0) (THead (Bind x1) x2 x3) H16:eq T t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)) H17:pr2 c x x5 H18:pr2 c x2 x6 H19:pr2 (CHead c (Bind x1) x6) x3 x4 ⇒
the thesis becomes sn3 c t3
(H21)
by (f_equal . . . . . H15)
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) t1 x0 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:T.B>
CASE THead (Bind x1) x2 x3 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq
B
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
THead (Bind b) t1 x0
λe:T
.<λ:T.B>
CASE e OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
THead (Bind x1) x2 x3
end of H21
(h1)
(H22)
by (f_equal . . . . . H15)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) t1 x0 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0 (THead (Bind b) t1 x0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0 (THead (Bind x1) x2 x3)
end of H22
(h1)
(H23)
by (f_equal . . . . . H15)
we proved
eq
T
<λ:T.T> CASE THead (Bind b) t1 x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0 (THead (Bind b) t1 x0)
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0 (THead (Bind x1) x2 x3)
end of H23
suppose H24: eq T t1 x2
suppose H25: eq B b x1
(H26)
consider H23
we proved
eq
T
<λ:T.T> CASE THead (Bind b) t1 x0 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
that is equivalent to eq T x0 x3
by (eq_ind_r . . . H19 . previous)
pr2 (CHead c (Bind x1) x6) x0 x4
end of H26
(H27)
by (eq_ind_r . . . H18 . H24)
pr2 c t1 x6
end of H27
(H28)
by (eq_ind_r . . . H26 . H25)
pr2 (CHead c (Bind b) x6) x0 x4
end of H28
we proceed by induction on H25 to prove sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Bind b) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
(h1)
(h1) by (sn3_sing . . H1) we proved sn3 c t1
(h2)
(H_x)
by (term_dec . .)
or (eq T x x5) (eq T x x5)→∀P:Prop.P
end of H_x
(H29) consider H_x
we proceed by induction on H29 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x5) x4)
case or_introl : H30:eq T x x5 ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x5) x4)
we proceed by induction on H30 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x5) x4)
case refl_equal : ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
(H_x0)
by (term_dec . .)
or (eq T x0 x4) (eq T x0 x4)→∀P:Prop.P
end of H_x0
(H32) consider H_x0
we proceed by induction on H32 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
case or_introl : H33:eq T x0 x4 ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
we proceed by induction on H33 to prove sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
case refl_equal : ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0)
by (sn3_sing . . H9)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
case or_intror : H33:(eq T x0 x4)→∀P:Prop.P ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
(h1)
suppose H34:
eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x) x4
assume P: Prop
(H35)
by (f_equal . . . . . H34)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x) x4
end of H35
(H36)
consider H35
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
that is equivalent to eq T x0 x4
by (eq_ind_r . . . H33 . previous)
(eq T x0 x0)→∀P0:Prop.P0
end of H36
by (refl_equal . .)
we proved eq T x0 x0
by (H36 previous .)
we proved P
(eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x) x4)
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr3_pr2 . . . H27) we proved pr3 c t1 x6
(h2)
by (pr2_thin_dx . . . H28 . .)
we proved
pr2
CHead c (Bind b) x6
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x) x4
by (pr3_pr2 . . . previous)
pr3
CHead c (Bind b) x6
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x) x4
end of h2
by (pr3_pr3_pr3_t . . . h1 . . . h2)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x) x4
end of h2
by (H9 . h1 h2)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x5) x4)
case or_intror : H30:(eq T x x5)→∀P:Prop.P ⇒
the thesis becomes sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x5) x4)
(h1)
suppose H31:
eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x5) x4
assume P: Prop
(H32)
by (f_equal . . . . . H31)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x5) x4 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| THead t0 ⇒t0
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| THead t0 ⇒t0
THead (Flat Appl) (lift (S O) O x5) x4
end of H32
(h1)
(H33)
by (f_equal . . . . . H31)
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x5) x4 OF
TSort ⇒x0
| TLRef ⇒x0
| THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x) x0
λe:T.<λ:T.T> CASE e OF TSort ⇒x0 | TLRef ⇒x0 | THead t0⇒t0
THead (Flat Appl) (lift (S O) O x5) x4
end of H33
suppose H34: eq T (lift (S O) O x) (lift (S O) O x5)
(H35)
by (lift_inj . . . . H34)
we proved eq T x x5
by (eq_ind_r . . . H30 . previous)
(eq T x x)→∀P0:Prop.P0
end of H35
by (refl_equal . .)
we proved eq T x x
by (H35 previous .)
we proved P
(eq T (lift (S O) O x) (lift (S O) O x5))→P
end of h1
(h2)
consider H32
we proved
eq
T
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x) x0 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| THead t0 ⇒t0
<λ:T.T>
CASE THead (Flat Appl) (lift (S O) O x5) x4 OF
TSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| TLRef ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd:nat
.λt0:T
.<λt4:T.T>
CASE t0 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d OF true⇒i | false⇒f i
| THead k u0 t4⇒THead k (lref_map f d u0) (lref_map f (s k d) t4)
}
λx7:nat.plus x7 (S O)
O
x
| THead t0 ⇒t0
eq T (lift (S O) O x) (lift (S O) O x5)
end of h2
by (h1 h2)
we proved P
(eq
T
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x5) x4)
→∀P:Prop.P
end of h1
(h2)
(h1) by (pr3_pr2 . . . H27) we proved pr3 c t1 x6
(h2)
(h1)
(h1)
by (drop_refl .)
we proved drop O O c c
that is equivalent to drop (r (Bind b) O) O c c
by (drop_drop . . . . previous .)
drop (S O) O (CHead c (Bind b) x6) c
end of h1
(h2) by (pr3_pr2 . . . H17) we proved pr3 c x x5
by (pr3_lift . . . . h1 . . h2)
pr3 (CHead c (Bind b) x6) (lift (S O) O x) (lift (S O) O x5)
end of h1
(h2)
by (pr3_pr2 . . . H28)
pr3 (CHead c (Bind b) x6) x0 x4
end of h2
by (pr3_flat . . . h1 . . h2 .)
pr3
CHead c (Bind b) x6
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x5) x4
end of h2
by (pr3_pr3_pr3_t . . . h1 . . . h2)
pr3
CHead c (Bind b) t1
THead (Flat Appl) (lift (S O) O x) x0
THead (Flat Appl) (lift (S O) O x5) x4
end of h2
by (H9 . h1 h2)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x5) x4)
sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x5) x4)
end of h2
by (sn3_bind . . . h1 . h2)
sn3 c (THead (Bind b) t1 (THead (Flat Appl) (lift (S O) O x5) x4))
end of h1
(h2)
by (pr2_head_1 . . . H27 . .)
we proved
pr2
c
THead (Bind b) t1 (THead (Flat Appl) (lift (S O) O x5) x4)
THead (Bind b) x6 (THead (Flat Appl) (lift (S O) O x5) x4)
by (pr3_pr2 . . . previous)
pr3
c
THead (Bind b) t1 (THead (Flat Appl) (lift (S O) O x5) x4)
THead (Bind b) x6 (THead (Flat Appl) (lift (S O) O x5) x4)
end of h2
by (sn3_pr3_trans . . h1 . h2)
sn3 c (THead (Bind b) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
we proved sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
eq T t1 x2
→(eq B b x1
→sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))
end of h1
(h2)
consider H22
we proved
eq
T
<λ:T.T> CASE THead (Bind b) t1 x0 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
<λ:T.T> CASE THead (Bind x1) x2 x3 OF TSort ⇒t1 | TLRef ⇒t1 | THead t0 ⇒t0
eq T t1 x2
end of h2
by (h1 h2)
eq B b x1
→sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
end of h1
(h2)
consider H21
we proved
eq
B
<λ:T.B>
CASE THead (Bind b) t1 x0 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
<λ:T.B>
CASE THead (Bind x1) x2 x3 OF
TSort ⇒b
| TLRef ⇒b
| THead k ⇒<λ:K.B> CASE k OF Bind b0⇒b0 | Flat ⇒b
eq B b x1
end of h2
by (h1 h2)
we proved sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
by (eq_ind_r . . . previous . H16)
sn3 c t3
sn3 c t3
we proved sn3 c t3
we proved
∀t3:T
.(eq T (THead (Flat Appl) x (THead (Bind b) t1 x0)) t3)→∀P:Prop.P
→(pr2 c (THead (Flat Appl) x (THead (Bind b) t1 x0)) t3)→(sn3 c t3)
by (sn3_pr2_intro . . previous)
we proved sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))
∀x:T
.∀x0:T
.∀H7:eq T t2 (THead (Flat Appl) (lift (S O) O x) x0)
.sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))
we proved
∀x:T
.∀x0:T
.eq T y (THead (Flat Appl) (lift (S O) O x) x0)
→sn3 c (THead (Flat Appl) x (THead (Bind b) t1 x0))
by (unintro . . . previous)
we proved
∀x:T
.eq T y (THead (Flat Appl) (lift (S O) O v) x)
→sn3 c (THead (Flat Appl) v (THead (Bind b) t1 x))
by (unintro . . . previous)
we proved
eq T y (THead (Flat Appl) (lift (S O) O v) t)
→sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t))
we proved
∀y:T
.sn3 (CHead c (Bind b) t1) y
→(eq T y (THead (Flat Appl) (lift (S O) O v) t)
→sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t)))
by (insert_eq . . . . previous H3)
we proved sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t))
∀t:T
.∀v:T
.∀H3:sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O v) t)
.sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t))
we proved
∀t0:T
.∀v:T
.sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O v) t0)
→sn3 c (THead (Flat Appl) v (THead (Bind b) u t0))
we proved
∀b:B
.not (eq B b Abst)
→∀c:C
.∀u:T
.sn3 c u
→∀t0:T
.∀v:T
.sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O v) t0)
→sn3 c (THead (Flat Appl) v (THead (Bind b) u t0))