DEFINITION drop_gen_skip_l()
TYPE =
∀c:C
.∀x:C
.∀u:T
.∀h:nat
.∀d:nat
.∀k:K
.drop h (S d) (CHead c k u) x
→(ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e)
BODY =
assume c: C
assume x: C
assume u: T
assume h: nat
assume d: nat
assume k: K
suppose H: drop h (S d) (CHead c k u) x
assume y: C
suppose H0: drop h (S d) y x
assume y0: nat
suppose H1: drop h y0 y x
we proceed by induction on H1 to prove
eq nat y0 (S d)
→(eq C y (CHead c k u)
→(ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e))
case drop_refl : c0:C ⇒
the thesis becomes
∀H2:eq nat O (S d)
.∀H3:eq C c0 (CHead c k u)
.ex3_2
C
T
λe:C.λv:T.eq C c0 (CHead e k v)
λ:C.λv:T.eq T u (lift O (r k d) v)
λe:C.λ:T.drop O (r k d) c e
suppose H2: eq nat O (S d)
suppose H3: eq C c0 (CHead c k u)
(H4)
we proceed by induction on H2 to prove <λ:nat.Prop> CASE S d OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S d OF O⇒True | S ⇒False
end of H4
consider H4
we proved <λ:nat.Prop> CASE S d OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
C
T
λe:C.λv:T.eq C (CHead c k u) (CHead e k v)
λ:C.λv:T.eq T u (lift O (r k d) v)
λe:C.λ:T.drop O (r k d) c e
we proved
ex3_2
C
T
λe:C.λv:T.eq C (CHead c k u) (CHead e k v)
λ:C.λv:T.eq T u (lift O (r k d) v)
λe:C.λ:T.drop O (r k d) c e
by (eq_ind_r . . . previous . H3)
we proved
ex3_2
C
T
λe:C.λv:T.eq C c0 (CHead e k v)
λ:C.λv:T.eq T u (lift O (r k d) v)
λe:C.λ:T.drop O (r k d) c e
∀H2:eq nat O (S d)
.∀H3:eq C c0 (CHead c k u)
.ex3_2
C
T
λe:C.λv:T.eq C c0 (CHead e k v)
λ:C.λv:T.eq T u (lift O (r k d) v)
λe:C.λ:T.drop O (r k d) c e
case drop_drop : k0:K h0:nat c0:C e:C H2:drop (r k0 h0) O c0 e u0:T ⇒
the thesis becomes
∀H4:eq nat O (S d)
.∀H5:eq C (CHead c0 k0 u0) (CHead c k u)
.ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (S h0) (r k d) v)
λe0:C.λ:T.drop (S h0) (r k d) c e0
(H3) by induction hypothesis we know
eq nat O (S d)
→(eq C c0 (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (r k0 h0) (r k d) v)
λe0:C.λ:T.drop (r k0 h0) (r k d) c e0))
suppose H4: eq nat O (S d)
suppose H5: eq C (CHead c0 k0 u0) (CHead c k u)
(H6)
by (f_equal . . . . . H5)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c0 k0 u0)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c k u)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 u0)
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c k u)
end of H7
(H9)
consider H7
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of H9
suppose H10: eq C c0 c
(H11)
we proceed by induction on H10 to prove
eq nat O (S d)
→(eq C c (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (r k0 h0) (r k d) v)
λe0:C.λ:T.drop (r k0 h0) (r k d) c e0))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq nat O (S d)
→(eq C c (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (r k0 h0) (r k d) v)
λe0:C.λ:T.drop (r k0 h0) (r k d) c e0))
end of H11
(H12)
we proceed by induction on H10 to prove drop (r k0 h0) O c e
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop (r k0 h0) O c e
end of H12
(H15)
we proceed by induction on H4 to prove <λ:nat.Prop> CASE S d OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S d OF O⇒True | S ⇒False
end of H15
consider H15
we proved <λ:nat.Prop> CASE S d OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (S h0) (r k d) v)
λe0:C.λ:T.drop (S h0) (r k d) c e0
we proved
ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (S h0) (r k d) v)
λe0:C.λ:T.drop (S h0) (r k d) c e0
eq C c0 c
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (S h0) (r k d) v)
λe0:C.λ:T.drop (S h0) (r k d) c e0)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq C c0 c
end of h2
by (h1 h2)
we proved
ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (S h0) (r k d) v)
λe0:C.λ:T.drop (S h0) (r k d) c e0
∀H4:eq nat O (S d)
.∀H5:eq C (CHead c0 k0 u0) (CHead c k u)
.ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift (S h0) (r k d) v)
λe0:C.λ:T.drop (S h0) (r k d) c e0
case drop_skip : k0:K h0:nat d0:nat c0:C e:C H2:drop h0 (r k0 d0) c0 e u0:T ⇒
the thesis becomes
∀H4:eq nat (S d0) (S d)
.∀H5:eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k u)
.ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k0 u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
(H3) by induction hypothesis we know
eq nat (r k0 d0) (S d)
→(eq C c0 (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0))
suppose H4: eq nat (S d0) (S d)
suppose H5: eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k u)
(H6)
by (f_equal . . . . . H5)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 (lift h0 (r k0 d0) u0) OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c0 k0 (lift h0 (r k0 d0) u0))
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c k u)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 (lift h0 (r k0 d0) u0) OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 (lift h0 (r k0 d0) u0))
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c k u)
end of H7
(h1)
(H8)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:C.T>
CASE CHead c0 k0 (lift h0 (r k0 d0) u0) OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd1:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d1 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d1 u1) (lref_map f (s k1 d1) t0)
}
λx0:nat.plus x0 h0
r k0 d0
u0
| CHead t⇒t
<λ:C.T>
CASE CHead c k u OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd1:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d1 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d1 u1) (lref_map f (s k1 d1) t0)
}
λx0:nat.plus x0 h0
r k0 d0
u0
| CHead t⇒t
eq
T
λe0:C
.<λ:C.T>
CASE e0 OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd1:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d1 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d1 u1) (lref_map f (s k1 d1) t0)
}
λx0:nat.plus x0 h0
r k0 d0
u0
| CHead t⇒t
CHead c0 k0 (lift h0 (r k0 d0) u0)
λe0:C
.<λ:C.T>
CASE e0 OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd1:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d1 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d1 u1) (lref_map f (s k1 d1) t0)
}
λx0:nat.plus x0 h0
r k0 d0
u0
| CHead t⇒t
CHead c k u
end of H8
suppose H9: eq K k0 k
suppose H10: eq C c0 c
(H11)
we proceed by induction on H10 to prove
eq nat (r k0 d0) (S d)
→(eq C c (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq nat (r k0 d0) (S d)
→(eq C c (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0))
end of H11
(H12)
we proceed by induction on H10 to prove drop h0 (r k0 d0) c e
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop h0 (r k0 d0) c e
end of H12
(H13)
we proceed by induction on H9 to prove eq T (lift h0 (r k d0) u0) u
case refl_equal : ⇒
the thesis becomes eq T (lift h0 (r k0 d0) u0) u
consider H8
we proved
eq
T
<λ:C.T>
CASE CHead c0 k0 (lift h0 (r k0 d0) u0) OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd1:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d1 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d1 u1) (lref_map f (s k1 d1) t0)
}
λx0:nat.plus x0 h0
r k0 d0
u0
| CHead t⇒t
<λ:C.T>
CASE CHead c k u OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd1:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d1 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d1 u1) (lref_map f (s k1 d1) t0)
}
λx0:nat.plus x0 h0
r k0 d0
u0
| CHead t⇒t
eq T (lift h0 (r k0 d0) u0) u
eq T (lift h0 (r k d0) u0) u
end of H13
(H14)
we proceed by induction on H9 to prove
eq nat (r k d0) (S d)
→(eq C c (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0))
case refl_equal : ⇒
the thesis becomes the hypothesis H11
eq nat (r k d0) (S d)
→(eq C c (CHead c k u)
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0))
end of H14
(H15)
we proceed by induction on H9 to prove drop h0 (r k d0) c e
case refl_equal : ⇒
the thesis becomes the hypothesis H12
drop h0 (r k d0) c e
end of H15
(H16)
by (eq_ind_r . . . H14 . H13)
eq nat (r k d0) (S d)
→(eq C c (CHead c k (lift h0 (r k d0) u0))
→(ex3_2
C
T
λe0:C.λv:T.eq C e (CHead e0 k v)
λ:C.λv:T.eq T (lift h0 (r k d0) u0) (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0))
end of H16
we proceed by induction on H13 to prove
ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
case refl_equal : ⇒
the thesis becomes
ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k u0) (CHead e0 k v)
λ:C.λv:T.eq T (lift h0 (r k d0) u0) (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
(H17)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:nat.nat> CASE S d0 OF O⇒d0 | S n⇒n
<λ:nat.nat> CASE S d OF O⇒d0 | S n⇒n
eq
nat
λe0:nat.<λ:nat.nat> CASE e0 OF O⇒d0 | S n⇒n (S d0)
λe0:nat.<λ:nat.nat> CASE e0 OF O⇒d0 | S n⇒n (S d)
end of H17
(H19)
consider H17
we proved
eq
nat
<λ:nat.nat> CASE S d0 OF O⇒d0 | S n⇒n
<λ:nat.nat> CASE S d OF O⇒d0 | S n⇒n
that is equivalent to eq nat d0 d
we proceed by induction on the previous result to prove drop h0 (r k d) c e
case refl_equal : ⇒
the thesis becomes the hypothesis H15
drop h0 (r k d) c e
end of H19
(h1)
(h1)
by (refl_equal . .)
eq C (CHead e k u0) (CHead e k u0)
end of h1
(h2)
by (refl_equal . .)
eq T (lift h0 (r k d) u0) (lift h0 (r k d) u0)
end of h2
by (ex3_2_intro . . . . . . . h1 h2 H19)
ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k u0) (CHead e0 k v)
λ:C.λv:T.eq T (lift h0 (r k d) u0) (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
end of h1
(h2)
consider H17
we proved
eq
nat
<λ:nat.nat> CASE S d0 OF O⇒d0 | S n⇒n
<λ:nat.nat> CASE S d OF O⇒d0 | S n⇒n
eq nat d0 d
end of h2
by (eq_ind_r . . . h1 . h2)
ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k u0) (CHead e0 k v)
λ:C.λv:T.eq T (lift h0 (r k d0) u0) (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
we proved
ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
by (eq_ind_r . . . previous . H9)
we proved
ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k0 u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
eq K k0 k
→(eq C c0 c
→(ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k0 u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0))
end of h1
(h2)
consider H7
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 (lift h0 (r k0 d0) u0) OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
eq C c0 c
→(ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k0 u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 (lift h0 (r k0 d0) u0) OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq C c0 c
end of h2
by (h1 h2)
we proved
ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k0 u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
∀H4:eq nat (S d0) (S d)
.∀H5:eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k u)
.ex3_2
C
T
λe0:C.λv:T.eq C (CHead e k0 u0) (CHead e0 k v)
λ:C.λv:T.eq T u (lift h0 (r k d) v)
λe0:C.λ:T.drop h0 (r k d) c e0
we proved
eq nat y0 (S d)
→(eq C y (CHead c k u)
→(ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e))
we proved
∀y0:nat
.drop h y0 y x
→(eq nat y0 (S d)
→(eq C y (CHead c k u)
→(ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e)))
by (insert_eq . . . . previous H0)
we proved
eq C y (CHead c k u)
→(ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e)
we proved
∀y:C
.drop h (S d) y x
→(eq C y (CHead c k u)
→(ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e))
by (insert_eq . . . . previous H)
we proved
ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e
we proved
∀c:C
.∀x:C
.∀u:T
.∀h:nat
.∀d:nat
.∀k:K
.drop h (S d) (CHead c k u) x
→(ex3_2
C
T
λe:C.λv:T.eq C x (CHead e k v)
λ:C.λv:T.eq T u (lift h (r k d) v)
λe:C.λ:T.drop h (r k d) c e)