DEFINITION thead_x_lift_y_y()
TYPE =
∀k:K.∀t:T.∀v:T.∀h:nat.∀d:nat.(eq T (THead k v (lift h d t)) t)→∀P:Prop.P
BODY =
assume k: K
assume t: T
we proceed by induction on t to prove ∀v:T.∀h:nat.∀d:nat.(eq T (THead k v (lift h d t)) t)→∀P:Prop.P
case TSort : n:nat ⇒
the thesis becomes
∀v:T
.∀h:nat
.∀d:nat.∀H:(eq T (THead k v (lift h d (TSort n))) (TSort n)).∀P:Prop.P
assume v: T
assume h: nat
assume d: nat
suppose H: eq T (THead k v (lift h 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 k v (lift h d (TSort n)) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k v (lift h 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
∀v:T
.∀h:nat
.∀d:nat.∀H:(eq T (THead k v (lift h d (TSort n))) (TSort n)).∀P:Prop.P
case TLRef : n:nat ⇒
the thesis becomes
∀v:T
.∀h:nat
.∀d:nat.∀H:(eq T (THead k v (lift h d (TLRef n))) (TLRef n)).∀P:Prop.P
assume v: T
assume h: nat
assume d: nat
suppose H: eq T (THead k v (lift h 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 k v (lift h d (TLRef n)) OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k v (lift h 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
∀v:T
.∀h:nat
.∀d:nat.∀H:(eq T (THead k v (lift h d (TLRef n))) (TLRef n)).∀P:Prop.P
case THead : k0:K t0:T t1:T ⇒
the thesis becomes
∀v:T
.∀h:nat.∀d:nat.∀H1:(eq T (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1)).∀P:Prop.P
() by induction hypothesis we know ∀v:T.∀h:nat.∀d:nat.(eq T (THead k v (lift h d t0)) t0)→∀P:Prop.P
(H0) by induction hypothesis we know ∀v:T.∀h:nat.∀d:nat.(eq T (THead k v (lift h d t1)) t1)→∀P:Prop.P
assume v: T
assume h: nat
assume d: nat
suppose H1: eq T (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1)
assume P: Prop
(H2)
by (f_equal . . . . . H1)
we proved
eq
K
<λ:T.K>
CASE THead k v (lift h d (THead k0 t0 t1)) OF
TSort ⇒k
| TLRef ⇒k
| THead k1 ⇒k1
<λ:T.K> CASE THead k0 t0 t1 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
THead k v (lift h d (THead k0 t0 t1))
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1 (THead k0 t0 t1)
end of H2
(h1)
(H3)
by (f_equal . . . . . H1)
we proved
eq
T
<λ:T.T>
CASE THead k v (lift h d (THead k0 t0 t1)) OF
TSort ⇒v
| TLRef ⇒v
| THead t2 ⇒t2
<λ:T.T> CASE THead k0 t0 t1 OF TSort ⇒v | TLRef ⇒v | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒v | TLRef ⇒v | THead t2 ⇒t2
THead k v (lift h d (THead k0 t0 t1))
λe:T.<λ:T.T> CASE e OF TSort ⇒v | TLRef ⇒v | THead t2 ⇒t2 (THead k0 t0 t1)
end of H3
(h1)
(H4)
by (f_equal . . . . . H1)
we proved
eq
T
<λ:T.T>
CASE THead k v (lift h d (THead k0 t0 t1)) OF
TSort ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| TLRef ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| THead t2⇒t2
<λ:T.T>
CASE THead k0 t0 t1 OF
TSort ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| TLRef ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| THead t2⇒t2
eq
T
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| TLRef ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| THead t2⇒t2
THead k v (lift h d (THead k0 t0 t1))
λe:T
.<λ:T.T>
CASE e OF
TSort ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| TLRef ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| THead t2⇒t2
THead k0 t0 t1
end of H4
suppose : eq T v t0
suppose H6: eq K k k0
(H7)
we proceed by induction on H6 to prove ∀v0:T.∀h0:nat.∀d0:nat.(eq T (THead k0 v0 (lift h0 d0 t1)) t1)→∀P0:Prop.P0
case refl_equal : ⇒
the thesis becomes the hypothesis H0
∀v0:T.∀h0:nat.∀d0:nat.(eq T (THead k0 v0 (lift h0 d0 t1)) t1)→∀P0:Prop.P0
end of H7
(H8)
by (lift_head . . . . .)
we proved eq T (lift h d (THead k0 t0 t1)) (THead k0 (lift h d t0) (lift h (s k0 d) t1))
we proceed by induction on the previous result to prove eq T (THead k0 (lift h d t0) (lift h (s k0 d) t1)) t1
case refl_equal : ⇒
the thesis becomes eq T (lift h d (THead k0 t0 t1)) t1
consider H4
we proved
eq
T
<λ:T.T>
CASE THead k v (lift h d (THead k0 t0 t1)) OF
TSort ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| TLRef ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| THead t2⇒t2
<λ:T.T>
CASE THead k0 t0 t1 OF
TSort ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| TLRef ⇒
THead
k0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
d
t0
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt2:T
.<λt3:T.T>
CASE t2 OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u t3⇒THead k1 (lref_map f d0 u) (lref_map f (s k1 d0) t3)
}
λx:nat.plus x h
s k0 d
t1
| THead t2⇒t2
eq T (lift h d (THead k0 t0 t1)) t1
eq T (THead k0 (lift h d t0) (lift h (s k0 d) t1)) t1
end of H8
by (H7 . . . H8 .)
we proved P
(eq T v t0)→(eq K k k0)→P
end of h1
(h2)
consider H3
we proved
eq
T
<λ:T.T>
CASE THead k v (lift h d (THead k0 t0 t1)) OF
TSort ⇒v
| TLRef ⇒v
| THead t2 ⇒t2
<λ:T.T> CASE THead k0 t0 t1 OF TSort ⇒v | TLRef ⇒v | THead t2 ⇒t2
eq T v t0
end of h2
by (h1 h2)
(eq K k k0)→P
end of h1
(h2)
consider H2
we proved
eq
K
<λ:T.K>
CASE THead k v (lift h d (THead k0 t0 t1)) OF
TSort ⇒k
| TLRef ⇒k
| THead k1 ⇒k1
<λ:T.K> CASE THead k0 t0 t1 OF TSort ⇒k | TLRef ⇒k | THead k1 ⇒k1
eq K k k0
end of h2
by (h1 h2)
we proved P
∀v:T
.∀h:nat.∀d:nat.∀H1:(eq T (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1)).∀P:Prop.P
we proved ∀v:T.∀h:nat.∀d:nat.(eq T (THead k v (lift h d t)) t)→∀P:Prop.P
we proved ∀k:K.∀t:T.∀v:T.∀h:nat.∀d:nat.(eq T (THead k v (lift h d t)) t)→∀P:Prop.P