DEFINITION nf2_gen__nf2_gen_aux()
TYPE =
∀b:B
.∀x:T
.∀u:T.∀d:nat.(eq T (THead (Bind b) u (lift (S O) d x)) x)→∀P:Prop.P
BODY =
assume b: B
assume x: T
we proceed by induction on x to prove
∀u:T.∀d:nat.(eq T (THead (Bind b) u (lift (S O) d x)) x)→∀P:Prop.P
case TSort : n:nat ⇒
the thesis becomes
∀u:T
.∀d:nat
.∀H:eq T (THead (Bind b) u (lift (S O) d (TSort n))) (TSort n)
.∀P:Prop.P
assume u: T
assume d: nat
suppose H: eq T (THead (Bind b) u (lift (S O) d (TSort n))) (TSort n)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) d (TSort n)) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) d (TSort n)) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H0
consider H0
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
∀u:T
.∀d:nat
.∀H:eq T (THead (Bind b) u (lift (S O) d (TSort n))) (TSort n)
.∀P:Prop.P
case TLRef : n:nat ⇒
the thesis becomes
∀u:T
.∀d:nat
.∀H:eq T (THead (Bind b) u (lift (S O) d (TLRef n))) (TLRef n)
.∀P:Prop.P
assume u: T
assume d: nat
suppose H: eq T (THead (Bind b) u (lift (S O) d (TLRef n))) (TLRef n)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) d (TLRef n)) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u (lift (S O) d (TLRef n)) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H0
consider H0
we proved
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
∀u:T
.∀d:nat
.∀H:eq T (THead (Bind b) u (lift (S O) d (TLRef n))) (TLRef n)
.∀P:Prop.P
case THead : k:K t:T t0:T ⇒
the thesis becomes
∀u:T
.∀d:nat
.∀H1:eq
T
THead (Bind b) u (lift (S O) d (THead k t t0))
THead k t t0
.∀P:Prop.P
() by induction hypothesis we know
∀u:T.∀d:nat.(eq T (THead (Bind b) u (lift (S O) d t)) t)→∀P:Prop.P
(H0) by induction hypothesis we know ∀u:T.∀d:nat.(eq T (THead (Bind b) u (lift (S O) d t0)) t0)→∀P:Prop.P
assume u: T
assume d: nat
suppose H1:
eq
T
THead (Bind b) u (lift (S O) d (THead k t t0))
THead k t t0
assume P: Prop
(H2)
by (f_equal . . . . . H1)
we proved
eq
K
<λ:T.K>
CASE THead (Bind b) u (lift (S O) d (THead k t t0)) OF
TSort ⇒Bind b
| TLRef ⇒Bind b
| THead k0 ⇒k0
<λ:T.K>
CASE THead k t t0 OF
TSort ⇒Bind b
| TLRef ⇒Bind b
| THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒Bind b | TLRef ⇒Bind b | THead k0 ⇒k0
THead (Bind b) u (lift (S O) d (THead k t t0))
λe:T.<λ:T.K> CASE e OF TSort ⇒Bind b | TLRef ⇒Bind b | THead k0 ⇒k0
THead k t t0
end of H2
(h1)
(H3)
by (f_equal . . . . . H1)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b) u (lift (S O) d (THead k t t0)) OF
TSort ⇒u
| TLRef ⇒u
| THead t1 ⇒t1
<λ:T.T> CASE THead k t t0 OF TSort ⇒u | TLRef ⇒u | THead t1 ⇒t1
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t1 ⇒t1
THead (Bind b) u (lift (S O) d (THead k t t0))
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t1 ⇒t1 (THead k t t0)
end of H3
(h1)
(H4)
by (f_equal . . . . . H1)
we proved
eq
T
<λ:T.T>
CASE THead (Bind b) u (lift (S O) d (THead k t t0)) OF
TSort ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| TLRef ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| THead t1⇒t1
<λ:T.T>
CASE THead k t t0 OF
TSort ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| TLRef ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| THead t1⇒t1
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| TLRef ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| THead t1⇒t1
THead (Bind b) u (lift (S O) d (THead k t t0))
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| TLRef ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| THead t1⇒t1
THead k t t0
end of H4
suppose : eq T u t
suppose H6: eq K (Bind b) k
(H7)
consider H4
we proved
eq
T
<λ:T.T>
CASE THead (Bind b) u (lift (S O) d (THead k t t0)) OF
TSort ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| TLRef ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| THead t1⇒t1
<λ:T.T>
CASE THead k t t0 OF
TSort ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| TLRef ⇒
THead
k
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
d
t
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt1:T
.<λt2:T.T>
CASE t1 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb1:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k0 u0 t2⇒THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2)
}
λx0:nat.plus x0 (S O)
s k d
t0
| THead t1⇒t1
that is equivalent to eq T (lift (S O) d (THead k t t0)) t0
by (eq_ind_r . . . previous . H6)
eq T (lift (S O) d (THead (Bind b) t t0)) t0
end of H7
(H8)
by (lift_bind . . . . .)
we proved
eq
T
lift (S O) d (THead (Bind b) t t0)
THead (Bind b) (lift (S O) d t) (lift (S O) (S d) t0)
we proceed by induction on the previous result to prove eq T (THead (Bind b) (lift (S O) d t) (lift (S O) (S d) t0)) t0
case refl_equal : ⇒
the thesis becomes the hypothesis H7
eq T (THead (Bind b) (lift (S O) d t) (lift (S O) (S d) t0)) t0
end of H8
by (H0 . . H8 .)
we proved P
(eq T u t)→(eq K (Bind b) k)→P
end of h1
(h2)
consider H3
we proved
eq
T
<λ:T.T>
CASE THead (Bind b) u (lift (S O) d (THead k t t0)) OF
TSort ⇒u
| TLRef ⇒u
| THead t1 ⇒t1
<λ:T.T> CASE THead k t t0 OF TSort ⇒u | TLRef ⇒u | THead t1 ⇒t1
eq T u t
end of h2
by (h1 h2)
(eq K (Bind b) k)→P
end of h1
(h2)
consider H2
we proved
eq
K
<λ:T.K>
CASE THead (Bind b) u (lift (S O) d (THead k t t0)) OF
TSort ⇒Bind b
| TLRef ⇒Bind b
| THead k0 ⇒k0
<λ:T.K>
CASE THead k t t0 OF
TSort ⇒Bind b
| TLRef ⇒Bind b
| THead k0 ⇒k0
eq K (Bind b) k
end of h2
by (h1 h2)
we proved P
∀u:T
.∀d:nat
.∀H1:eq
T
THead (Bind b) u (lift (S O) d (THead k t t0))
THead k t t0
.∀P:Prop.P
we proved
∀u:T.∀d:nat.(eq T (THead (Bind b) u (lift (S O) d x)) x)→∀P:Prop.P
we proved
∀b:B
.∀x:T
.∀u:T.∀d:nat.(eq T (THead (Bind b) u (lift (S O) d x)) x)→∀P:Prop.P