DEFINITION drop_gen_skip_r()
TYPE =
∀c:C
.∀x:C
.∀u:T
.∀h:nat
.∀d:nat
.∀k:K
.drop h (S d) x (CHead c k u)
→(ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c)
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) x (CHead c k u)
assume y: C
suppose H0: drop h (S d) x y
assume y0: nat
suppose H1: drop h y0 x y
we proceed by induction on H1 to prove
eq nat y0 (S d)
→(eq C y (CHead c k u)
→(ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c))
case drop_refl : c0:C ⇒
the thesis becomes
∀H2:eq nat O (S d)
.∀H3:eq C c0 (CHead c k u)
.ex2 C λe:C.eq C c0 (CHead e k (lift O (r k d) u)) λe:C.drop O (r k d) e c
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
ex2
C
λe:C.eq C (CHead c k u) (CHead e k (lift O (r k d) u))
λe:C.drop O (r k d) e c
we proved
ex2
C
λe:C.eq C (CHead c k u) (CHead e k (lift O (r k d) u))
λe:C.drop O (r k d) e c
by (eq_ind_r . . . previous . H3)
we proved
ex2 C λe:C.eq C c0 (CHead e k (lift O (r k d) u)) λe:C.drop O (r k d) e c
∀H2:eq nat O (S d)
.∀H3:eq C c0 (CHead c k u)
.ex2 C λe:C.eq C c0 (CHead e k (lift O (r k d) u)) λe:C.drop O (r k d) e c
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 e (CHead c k u)
.ex2
C
λe0:C.eq C (CHead c0 k0 u0) (CHead e0 k (lift (S h0) (r k d) u))
λe0:C.drop (S h0) (r k d) e0 c
(H3) by induction hypothesis we know
eq nat O (S d)
→(eq C e (CHead c k u)
→(ex2
C
λe0:C.eq C c0 (CHead e0 k (lift (r k0 h0) (r k d) u))
λe0:C.drop (r k0 h0) (r k d) e0 c))
suppose H4: eq nat O (S d)
suppose H5: eq C e (CHead c k u)
(H8)
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 H8
consider H8
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
ex2
C
λe0:C.eq C (CHead c0 k0 u0) (CHead e0 k (lift (S h0) (r k d) u))
λe0:C.drop (S h0) (r k d) e0 c
we proved
ex2
C
λe0:C.eq C (CHead c0 k0 u0) (CHead e0 k (lift (S h0) (r k d) u))
λe0:C.drop (S h0) (r k d) e0 c
∀H4:eq nat O (S d)
.∀H5:eq C e (CHead c k u)
.ex2
C
λe0:C.eq C (CHead c0 k0 u0) (CHead e0 k (lift (S h0) (r k d) u))
λe0:C.drop (S h0) (r k d) e0 c
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 e k0 u0) (CHead c k u)
.ex2
C
λe0:C.eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c
(H3) by induction hypothesis we know
eq nat (r k0 d0) (S d)
→(eq C e (CHead c k u)
→ex2 C λe0:C.eq C c0 (CHead e0 k (lift h0 (r k d) u)) λe0:C.drop h0 (r k d) e0 c)
suppose H4: eq nat (S d0) (S d)
suppose H5: eq C (CHead e k0 u0) (CHead c k u)
(H6)
by (f_equal . . . . . H5)
we proved
eq
C
<λ:C.C> CASE CHead e k0 u0 OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒e | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead e k0 u0)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead c k u)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:C.K> CASE CHead e 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 e k0 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 e k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c k u OF CSort ⇒u0 | CHead t⇒t
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u0 | CHead t⇒t (CHead e k0 u0)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u0 | CHead t⇒t (CHead c k u)
end of H8
suppose H9: eq K k0 k
suppose H10: eq C e c
(h1)
(H11)
we proceed by induction on H10 to prove
eq nat (r k0 d0) (S d)
→(eq C c (CHead c k u)
→ex2 C λe0:C.eq C c0 (CHead e0 k (lift h0 (r k d) u)) λe0:C.drop h0 (r k d) e0 c)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq nat (r k0 d0) (S d)
→(eq C c (CHead c k u)
→ex2 C λe0:C.eq C c0 (CHead e0 k (lift h0 (r k d) u)) λe0:C.drop h0 (r k d) e0 c)
end of H11
(H12)
we proceed by induction on H10 to prove drop h0 (r k0 d0) c0 c
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop h0 (r k0 d0) c0 c
end of H12
(H13)
we proceed by induction on H9 to prove
eq nat (r k d0) (S d)
→(eq C c (CHead c k u)
→ex2 C λe0:C.eq C c0 (CHead e0 k (lift h0 (r k d) u)) λe0:C.drop h0 (r k d) e0 c)
case refl_equal : ⇒
the thesis becomes the hypothesis H11
eq nat (r k d0) (S d)
→(eq C c (CHead c k u)
→ex2 C λe0:C.eq C c0 (CHead e0 k (lift h0 (r k d) u)) λe0:C.drop h0 (r k d) e0 c)
end of H13
(H14)
we proceed by induction on H9 to prove drop h0 (r k d0) c0 c
case refl_equal : ⇒
the thesis becomes the hypothesis H12
drop h0 (r k d0) c0 c
end of H14
(H15)
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 H15
(H17)
consider H15
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) c0 c
case refl_equal : ⇒
the thesis becomes the hypothesis H14
drop h0 (r k d) c0 c
end of H17
(h1)
by (refl_equal . .)
we proved eq C (CHead c0 k (lift h0 (r k d) u)) (CHead c0 k (lift h0 (r k d) u))
by (ex_intro2 . . . . previous H17)
ex2
C
λe0:C.eq C (CHead c0 k (lift h0 (r k d) u)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c
end of h1
(h2)
consider H15
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)
we proved
ex2
C
λe0:C.eq C (CHead c0 k (lift h0 (r k d0) u)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c
by (eq_ind_r . . . previous . H9)
ex2
C
λe0:C.eq C (CHead c0 k0 (lift h0 (r k0 d0) u)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c
end of h1
(h2)
consider H8
we proved
eq
T
<λ:C.T> CASE CHead e k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c k u OF CSort ⇒u0 | CHead t⇒t
eq T u0 u
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex2
C
λe0:C.eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c
eq K k0 k
→(eq C e c
→(ex2
C
λe0:C.eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c))
end of h1
(h2)
consider H7
we proved
eq
K
<λ:C.K> CASE CHead e 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 h2
by (h1 h2)
eq C e c
→(ex2
C
λe0:C.eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c)
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead e k0 u0 OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒e | CHead c1 ⇒c1
eq C e c
end of h2
by (h1 h2)
we proved
ex2
C
λe0:C.eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c
∀H4:eq nat (S d0) (S d)
.∀H5:eq C (CHead e k0 u0) (CHead c k u)
.ex2
C
λe0:C.eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead e0 k (lift h0 (r k d) u))
λe0:C.drop h0 (r k d) e0 c
we proved
eq nat y0 (S d)
→(eq C y (CHead c k u)
→(ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c))
we proved
∀y0:nat
.drop h y0 x y
→(eq nat y0 (S d)
→(eq C y (CHead c k u)
→(ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c)))
by (insert_eq . . . . previous H0)
we proved
eq C y (CHead c k u)
→(ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c)
we proved
∀y:C
.drop h (S d) x y
→(eq C y (CHead c k u)
→(ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c))
by (insert_eq . . . . previous H)
we proved
ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c
we proved
∀c:C
.∀x:C
.∀u:T
.∀h:nat
.∀d:nat
.∀k:K
.drop h (S d) x (CHead c k u)
→(ex2
C
λe:C.eq C x (CHead e k (lift h (r k d) u))
λe:C.drop h (r k d) e c)