DEFINITION getl_gen_tail()
TYPE =
∀k:K
.∀b:B
.∀u1:T
.∀u2:T
.∀c2:C
.∀c1:C
.∀i:nat
.getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
→(or
ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen c1)
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n))
BODY =
assume k: K
assume b: B
assume u1: T
assume u2: T
assume c2: C
assume c1: C
we proceed by induction on c1 to prove
∀i:nat
.getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
→(or
ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen c1)
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n))
case CSort : n:nat ⇒
the thesis becomes
∀i:nat
.getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
assume i: nat
we proceed by induction on i to prove
getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
case O : ⇒
the thesis becomes
getl O (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
we must prove
getl O (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
or equivalently
getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
suppose H: getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
by (getl_gen_O . . H)
we proved clear (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
assume b0: B
suppose H0: clear (CHead (CSort n) (Bind b0) u1) (CHead c2 (Bind b) u2)
(H1)
by (clear_gen_bind . . . . H0)
we proved eq C (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c ⇒c
<λ:C.C> CASE CHead (CSort n) (Bind b0) u1 OF CSort ⇒c2 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c ⇒c (CHead c2 (Bind b) u2)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c ⇒c
CHead (CSort n) (Bind b0) u1
end of H1
(h1)
(H2)
by (clear_gen_bind . . . . H0)
we proved eq C (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead (CSort n) (Bind b0) u1 OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead c2 (Bind b) u2
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead (CSort n) (Bind b0) u1
end of H2
(h1)
(H3)
by (clear_gen_bind . . . . H0)
we proved eq C (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead (CSort n) (Bind b0) u1 OF CSort ⇒u2 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t (CHead c2 (Bind b) u2)
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t
CHead (CSort n) (Bind b0) u1
end of H3
suppose H4: eq B b b0
suppose H5: eq C c2 (CSort n)
(h1)
(h1)
by (refl_equal . .)
eq nat O O
end of h1
(h2)
by (refl_equal . .)
eq K (Bind b0) (Bind b0)
end of h2
(h3)
by (refl_equal . .)
eq T u1 u1
end of h3
(h4)
by (refl_equal . .)
eq C (CSort n) (CSort n)
end of h4
by (ex4_intro . . . . . . h1 h2 h3 h4)
we proved
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b0)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort n) (CSort n0)
by (or_intror . . previous)
we proved
or
ex2
C
λe:C.eq C (CSort n) (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b0) u1)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b0)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort n) (CSort n0)
by (eq_ind_r . . . previous . H4)
or
ex2
C
λe:C.eq C (CSort n) (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort n) (CSort n0)
end of h1
(h2)
consider H3
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead (CSort n) (Bind b0) u1 OF CSort ⇒u2 | CHead t⇒t
eq T u2 u1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
ex2
C
λe:C.eq C (CSort n) (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C (CSort n) (CSort n0)
by (eq_ind_r . . . previous . H5)
we proved
or
ex2
C
λe:C.eq C c2 (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
eq B b b0
→(eq C c2 (CSort n)
→(or
ex2
C
λe:C.eq C c2 (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)))
end of h1
(h2)
consider H2
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead (CSort n) (Bind b0) u1 OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
eq B b b0
end of h2
by (h1 h2)
eq C c2 (CSort n)
→(or
ex2
C
λe:C.eq C c2 (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
end of h1
(h2)
consider H1
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c ⇒c
<λ:C.C> CASE CHead (CSort n) (Bind b0) u1 OF CSort ⇒c2 | CHead c ⇒c
eq C c2 (CSort n)
end of h2
by (h1 h2)
we proved
or
ex2
C
λe:C.eq C c2 (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
∀H0:clear (CHead (CSort n) (Bind b0) u1) (CHead c2 (Bind b) u2)
.or
ex2
C
λe:C.eq C c2 (CTail (Bind b0) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Bind b0) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
assume f: F
suppose H0: clear (CHead (CSort n) (Flat f) u1) (CHead c2 (Bind b) u2)
by (clear_gen_flat . . . . H0)
we proved clear (CSort n) (CHead c2 (Bind b) u2)
by (clear_gen_sort . . previous .)
we proved
or
ex2
C
λe:C.eq C c2 (CTail (Flat f) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Flat f) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
∀H0:clear (CHead (CSort n) (Flat f) u1) (CHead c2 (Bind b) u2)
.or
ex2
C
λe:C.eq C c2 (CTail (Flat f) u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K (Flat f) (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
by (previous . previous)
we proved
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O O
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
that is equivalent to
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1)
we proved
getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
getl O (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
case S : n0:nat ⇒
the thesis becomes
getl (S n0) (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n0) (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
() by induction hypothesis we know
getl n0 (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl n0 (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat n0 O
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
we must prove
getl (S n0) (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n0) (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
or equivalently
getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n0) (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
suppose H0: getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
by (getl_gen_S . . . . . H0)
we proved getl (r k n0) (CSort n) (CHead c2 (Bind b) u2)
by (getl_gen_sort . . . previous .)
we proved
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n0) O
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1)
that is equivalent to
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n0) (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1)
we proved
getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n0) (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
getl (S n0) (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n0) (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
we proved
getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
∀i:nat
.getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CSort n) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CSort n))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn1:nat.eq C c2 (CSort n1))
case CHead : c:C k0:K t:T ⇒
the thesis becomes
∀i:nat
.getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
(H) by induction hypothesis we know
∀i:nat
.getl i (CTail k u1 c) (CHead c2 (Bind b) u2)
→(or
ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen c)
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n))
assume i: nat
we proceed by induction on i to prove
getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
case O : ⇒
the thesis becomes
getl O (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
we must prove
getl O (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
or equivalently
getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
suppose H0: getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
by (getl_gen_O . . H0)
we proved clear (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
assume b0: B
suppose H1: clear (CHead (CTail k u1 c) (Bind b0) t) (CHead c2 (Bind b) u2)
(H2)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort ⇒c2 | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0 (CHead c2 (Bind b) u2)
λe:C.<λ:C.C> CASE e OF CSort ⇒c2 | CHead c0 ⇒c0
CHead (CTail k u1 c) (Bind b0) t
end of H2
(h1)
(H3)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead (CTail k u1 c) (Bind b0) t OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
eq
B
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
CHead c2 (Bind b) u2
λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
CHead (CTail k u1 c) (Bind b0) t
end of H3
(h1)
(H4)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort ⇒u2 | CHead t0⇒t0
<λ:C.T> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort ⇒u2 | CHead t0⇒t0
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t0⇒t0 (CHead c2 (Bind b) u2)
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t0⇒t0
CHead (CTail k u1 c) (Bind b0) t
end of H4
suppose H5: eq B b b0
suppose H6: eq C c2 (CTail k u1 c)
consider H4
we proved
eq
T
<λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort ⇒u2 | CHead t0⇒t0
<λ:C.T> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort ⇒u2 | CHead t0⇒t0
that is equivalent to eq T u2 t
we proceed by induction on the previous result to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
case refl_equal : ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) u2) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
we proceed by induction on H5 to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) u2) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
case refl_equal : ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
(h1)
by (refl_equal . .)
eq C (CTail k u1 c) (CTail k u1 c)
end of h1
(h2)
by (getl_refl . . .)
getl O (CHead c (Bind b) u2) (CHead c (Bind b) u2)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
C
λe:C.eq C (CTail k u1 c) (CTail k u1 e)
λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
by (or_introl . . previous)
we proved
or
ex2
C
λe:C.eq C (CTail k u1 c) (CTail k u1 e)
λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C (CTail k u1 c) (CSort n)
by (eq_ind_r . . . previous . H6)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) u2) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
we proved
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
eq B b b0
→(eq C c2 (CTail k u1 c)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)))
end of h1
(h2)
consider H3
we proved
eq
B
<λ:C.B>
CASE CHead c2 (Bind b) u2 OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead (CTail k u1 c) (Bind b0) t OF
CSort ⇒b
| CHead k1 ⇒<λ:K.B> CASE k1 OF Bind b1⇒b1 | Flat ⇒b
eq B b b0
end of h2
by (h1 h2)
eq C c2 (CTail k u1 c)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n))
end of h1
(h2)
consider H2
we proved
eq
C
<λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort ⇒c2 | CHead c0 ⇒c0
<λ:C.C> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort ⇒c2 | CHead c0 ⇒c0
eq C c2 (CTail k u1 c)
end of h2
by (h1 h2)
we proved
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
∀H1:clear (CHead (CTail k u1 c) (Bind b0) t) (CHead c2 (Bind b) u2)
.or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Bind b0) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
assume f: F
suppose H1: clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2 (Bind b) u2)
(H2)
(h1)
by (drop_refl .)
drop O O (CTail k u1 c) (CTail k u1 c)
end of h1
(h2)
by (clear_gen_flat . . . . H1)
clear (CTail k u1 c) (CHead c2 (Bind b) u2)
end of h2
by (getl_intro . . . . h1 h2)
we proved getl O (CTail k u1 c) (CHead c2 (Bind b) u2)
by (H . previous)
or
ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl O c (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen c)
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
end of H2
we proceed by induction on H2 to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
case or_introl : H3:ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl O c (CHead e (Bind b) u2) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
we proceed by induction on H3 to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
case ex_intro2 : x:C H4:eq C c2 (CTail k u1 x) H5:getl O c (CHead x (Bind b) u2) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
(h1)
by (refl_equal . .)
eq C (CTail k u1 x) (CTail k u1 x)
end of h1
(h2)
by (getl_flat . . . H5 . .)
getl O (CHead c (Flat f) t) (CHead x (Bind b) u2)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
C
λe:C.eq C (CTail k u1 x) (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
by (or_introl . . previous)
we proved
or
ex2
C
λe:C.eq C (CTail k u1 x) (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C (CTail k u1 x) (CSort n)
by (eq_ind_r . . . previous . H4)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
case or_intror : H3:ex4 nat λ:nat.eq nat O (clen c) λ:nat.eq K k (Bind b) λ:nat.eq T u1 u2 λn:nat.eq C c2 (CSort n) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
we proceed by induction on H3 to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
case ex4_intro : x0:nat H4:eq nat O (clen c) H5:eq K k (Bind b) H6:eq T u1 u2 H7:eq C c2 (CSort x0) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
we proceed by induction on H6 to prove
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C (CSort x0) (CSort n)
case refl_equal : ⇒
the thesis becomes
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u1
λn:nat.eq C (CSort x0) (CSort n)
(h1)
consider H4
we proved eq nat O (clen c)
eq nat O (s (Flat f) (clen c))
end of h1
(h2)
by (refl_equal . .)
eq K (Bind b) (Bind b)
end of h2
(h3)
by (refl_equal . .)
eq T u1 u1
end of h3
(h4)
by (refl_equal . .)
eq C (CSort x0) (CSort x0)
end of h4
by (ex4_intro . . . . . . h1 h2 h3 h4)
we proved
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn:nat.eq C (CSort x0) (CSort n)
by (or_intror . . previous)
we proved
or
ex2
C
λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn:nat.eq C (CSort x0) (CSort n)
by (eq_ind_r . . . previous . H5)
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u1
λn:nat.eq C (CSort x0) (CSort n)
we proved
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C (CSort x0) (CSort n)
by (eq_ind_r . . . previous . H7)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
we proved
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
∀H1:clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2 (Bind b) u2)
.or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s (Flat f) (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
by (previous . previous)
we proved
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
that is equivalent to
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
we proved
getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
getl O (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat O (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
case S : n:nat ⇒
the thesis becomes
getl (S n) (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
(H0) by induction hypothesis we know
getl n (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat n (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
we must prove
getl (S n) (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
or equivalently
getl (S n) (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
suppose H1: getl (S n) (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
(H_x)
by (getl_gen_S . . . . . H1)
we proved getl (r k0 n) (CTail k u1 c) (CHead c2 (Bind b) u2)
by (H . previous)
or
ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl (r k0 n) c (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (r k0 n) (clen c)
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
case or_introl : H3:ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl (r k0 n) c (CHead e (Bind b) u2) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
we proceed by induction on H3 to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
case ex_intro2 : x:C H4:eq C c2 (CTail k u1 x) H5:getl (r k0 n) c (CHead x (Bind b) u2) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
(h1)
by (refl_equal . .)
eq C (CTail k u1 x) (CTail k u1 x)
end of h1
(h2)
by (getl_head . . . . H5 .)
getl (S n) (CHead c k0 t) (CHead x (Bind b) u2)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
C
λe:C.eq C (CTail k u1 x) (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
by (or_introl . . previous)
we proved
or
ex2
C
λe:C.eq C (CTail k u1 x) (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C (CTail k u1 x) (CSort n0)
by (eq_ind_r . . . previous . H4)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
case or_intror : H3:ex4 nat λ:nat.eq nat (r k0 n) (clen c) λ:nat.eq K k (Bind b) λ:nat.eq T u1 u2 λn0:nat.eq C c2 (CSort n0) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
we proceed by induction on H3 to prove
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
case ex4_intro : x0:nat H4:eq nat (r k0 n) (clen c) H5:eq K k (Bind b) H6:eq T u1 u2 H7:eq C c2 (CSort x0) ⇒
the thesis becomes
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
(H8)
we proceed by induction on H7 to prove getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u2)
case refl_equal : ⇒
the thesis becomes getl (r k0 n) (CTail k u1 c) (CHead c2 (Bind b) u2)
by (getl_gen_S . . . . . H1)
getl (r k0 n) (CTail k u1 c) (CHead c2 (Bind b) u2)
getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u2)
end of H8
(H9)
we proceed by induction on H7 to prove
getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) u2)
→(or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat n (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C (CSort x0) (CSort n0))
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) u2)
→(or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat n (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C (CSort x0) (CSort n0))
end of H9
(H10)
by (eq_ind_r . . . H9 . H6)
getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) u1)
→(or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat n (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort x0) (CSort n0))
end of H10
(H11)
by (eq_ind_r . . . H8 . H6)
getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u1)
end of H11
we proceed by induction on H6 to prove
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C (CSort x0) (CSort n0)
case refl_equal : ⇒
the thesis becomes
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort x0) (CSort n0)
we proceed by induction on H4 to prove
or
ex2
C
λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn1:nat.eq C (CSort x0) (CSort n1)
case refl_equal : ⇒
the thesis becomes
or
ex2
C
λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat (S n) (s k0 (r k0 n))
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn1:nat.eq C (CSort x0) (CSort n1)
(h1)
(h1)
by (refl_equal . .)
eq nat (S n) (S n)
end of h1
(h2)
by (refl_equal . .)
eq K (Bind b) (Bind b)
end of h2
(h3)
by (refl_equal . .)
eq T u1 u1
end of h3
(h4)
by (refl_equal . .)
eq C (CSort x0) (CSort x0)
end of h4
by (ex4_intro . . . . . . h1 h2 h3 h4)
we proved
ex4
nat
λ:nat.eq nat (S n) (S n)
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort x0) (CSort n0)
by (or_intror . . previous)
or
ex2
C
λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat (S n) (S n)
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort x0) (CSort n0)
end of h1
(h2)
by (s_r . .)
eq nat (s k0 (r k0 n)) (S n)
end of h2
by (eq_ind_r . . . h1 . h2)
or
ex2
C
λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat (S n) (s k0 (r k0 n))
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn1:nat.eq C (CSort x0) (CSort n1)
we proved
or
ex2
C
λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K (Bind b) (Bind b)
λ:nat.eq T u1 u1
λn1:nat.eq C (CSort x0) (CSort n1)
by (eq_ind_r . . . previous . H5)
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u1
λn0:nat.eq C (CSort x0) (CSort n0)
we proved
or
ex2
C
λe:C.eq C (CSort x0) (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C (CSort x0) (CSort n0)
by (eq_ind_r . . . previous . H7)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
we proved
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (s k0 (clen c))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
that is equivalent to
or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0)
we proved
getl (S n) (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
getl (S n) (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat (S n) (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
we proved
getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
∀i:nat
.getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
→(or
ex2
C
λe:C.eq C c2 (CTail k u1 e)
λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen (CHead c k0 t))
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn0:nat.eq C c2 (CSort n0))
we proved
∀i:nat
.getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
→(or
ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen c1)
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n))
we proved
∀k:K
.∀b:B
.∀u1:T
.∀u2:T
.∀c2:C
.∀c1:C
.∀i:nat
.getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
→(or
ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
ex4
nat
λ:nat.eq nat i (clen c1)
λ:nat.eq K k (Bind b)
λ:nat.eq T u1 u2
λn:nat.eq C c2 (CSort n))