DEFINITION getl_flt()
TYPE =
∀b:B
.∀c:C
.∀e:C
.∀u:T
.∀i:nat.(getl i c (CHead e (Bind b) u))→(flt e u c (TLRef i))
BODY =
assume b: B
assume c: C
we proceed by induction on c to prove
∀e:C
.∀u:T
.∀i:nat.(getl i c (CHead e (Bind b) u))→(flt e u c (TLRef i))
case CSort : n:nat ⇒
the thesis becomes
∀e:C
.∀u:T
.∀i:nat
.∀H:getl i (CSort n) (CHead e (Bind b) u)
.flt e u (CSort n) (TLRef i)
assume e: C
assume u: T
assume i: nat
suppose H: getl i (CSort n) (CHead e (Bind b) u)
by (getl_gen_sort . . . H .)
we proved flt e u (CSort n) (TLRef i)
∀e:C
.∀u:T
.∀i:nat
.∀H:getl i (CSort n) (CHead e (Bind b) u)
.flt e u (CSort n) (TLRef i)
case CHead : c0:C k:K t:T ⇒
the thesis becomes
∀e:C
.∀u:T
.∀i:nat
.getl i (CHead c0 k t) (CHead e (Bind b) u)
→flt e u (CHead c0 k t) (TLRef i)
(H) by induction hypothesis we know
∀e:C
.∀u:T.∀i:nat.(getl i c0 (CHead e (Bind b) u))→(flt e u c0 (TLRef i))
assume e: C
assume u: T
assume i: nat
we proceed by induction on i to prove
getl i (CHead c0 k t) (CHead e (Bind b) u)
→flt e u (CHead c0 k t) (TLRef i)
case O : ⇒
the thesis becomes
getl O (CHead c0 k t) (CHead e (Bind b) u)
→flt e u (CHead c0 k t) (TLRef O)
suppose H0: getl O (CHead c0 k t) (CHead e (Bind b) u)
by (getl_gen_O . . H0)
we proved clear (CHead c0 k t) (CHead e (Bind b) u)
assume b0: B
suppose H1: clear (CHead c0 (Bind b0) t) (CHead e (Bind b) u)
(H2)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead e (Bind b) u) (CHead c0 (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead e (Bind b) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒e | CHead c1 ⇒c1 (CHead c0 (Bind b0) t)
end of H2
(h1)
(H3)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead e (Bind b) u) (CHead c0 (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
B
<λ:C.B>
CASE CHead e (Bind b) u OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c0 (Bind b0) t OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
eq
B
λe0:C.<λ:C.B> CASE e0 OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead e (Bind b) u
λe0:C.<λ:C.B> CASE e0 OF CSort ⇒b | CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
CHead c0 (Bind b0) t
end of H3
(h1)
(H4)
by (clear_gen_bind . . . . H1)
we proved eq C (CHead e (Bind b) u) (CHead c0 (Bind b0) t)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead e (Bind b) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c0 (Bind b0) t OF CSort ⇒u | CHead t0⇒t0
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t0⇒t0 (CHead e (Bind b) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t0⇒t0 (CHead c0 (Bind b0) t)
end of H4
suppose H5: eq B b b0
suppose H6: eq C e c0
(h1)
we proceed by induction on H5 to prove flt c0 t (CHead c0 (Bind b0) t) (TLRef O)
case refl_equal : ⇒
the thesis becomes flt c0 t (CHead c0 (Bind b) t) (TLRef O)
by (flt_arith0 . . . .)
flt c0 t (CHead c0 (Bind b) t) (TLRef O)
we proved flt c0 t (CHead c0 (Bind b0) t) (TLRef O)
by (eq_ind_r . . . previous . H6)
flt e t (CHead c0 (Bind b0) t) (TLRef O)
end of h1
(h2)
consider H4
we proved
eq
T
<λ:C.T> CASE CHead e (Bind b) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead c0 (Bind b0) t OF CSort ⇒u | CHead t0⇒t0
eq T u t
end of h2
by (eq_ind_r . . . h1 . h2)
we proved flt e u (CHead c0 (Bind b0) t) (TLRef O)
eq B b b0
→(eq C e c0)→(flt e u (CHead c0 (Bind b0) t) (TLRef O))
end of h1
(h2)
consider H3
we proved
eq
B
<λ:C.B>
CASE CHead e (Bind b) u OF
CSort ⇒b
| CHead k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
<λ:C.B>
CASE CHead c0 (Bind b0) t 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 e c0)→(flt e u (CHead c0 (Bind b0) t) (TLRef O))
end of h1
(h2)
consider H2
we proved
eq
C
<λ:C.C> CASE CHead e (Bind b) u OF CSort ⇒e | CHead c1 ⇒c1
<λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e | CHead c1 ⇒c1
eq C e c0
end of h2
by (h1 h2)
we proved flt e u (CHead c0 (Bind b0) t) (TLRef O)
∀H1:clear (CHead c0 (Bind b0) t) (CHead e (Bind b) u)
.flt e u (CHead c0 (Bind b0) t) (TLRef O)
assume f: F
suppose H1: clear (CHead c0 (Flat f) t) (CHead e (Bind b) u)
by (clear_gen_flat . . . . H1)
we proved clear c0 (CHead e (Bind b) u)
by (clear_cle . . previous)
we proved cle (CHead e (Bind b) u) c0
by (flt_arith1 . . . . previous . . .)
we proved flt e u (CHead c0 (Flat f) t) (TLRef O)
∀H1:clear (CHead c0 (Flat f) t) (CHead e (Bind b) u)
.flt e u (CHead c0 (Flat f) t) (TLRef O)
by (previous . previous)
we proved flt e u (CHead c0 k t) (TLRef O)
getl O (CHead c0 k t) (CHead e (Bind b) u)
→flt e u (CHead c0 k t) (TLRef O)
case S : n:nat ⇒
the thesis becomes
∀H1:getl (S n) (CHead c0 k t) (CHead e (Bind b) u)
.flt e u (CHead c0 k t) (TLRef (S n))
() by induction hypothesis we know
getl n (CHead c0 k t) (CHead e (Bind b) u)
→flt e u (CHead c0 k t) (TLRef n)
suppose H1: getl (S n) (CHead c0 k t) (CHead e (Bind b) u)
(H_y)
by (getl_gen_S . . . . . H1)
we proved getl (r k n) c0 (CHead e (Bind b) u)
by (H . . . previous)
flt e u c0 (TLRef (r k n))
end of H_y
by (flt_arith2 . . . . H_y . . .)
we proved flt e u (CHead c0 k t) (TLRef (S n))
∀H1:getl (S n) (CHead c0 k t) (CHead e (Bind b) u)
.flt e u (CHead c0 k t) (TLRef (S n))
we proved
getl i (CHead c0 k t) (CHead e (Bind b) u)
→flt e u (CHead c0 k t) (TLRef i)
∀e:C
.∀u:T
.∀i:nat
.getl i (CHead c0 k t) (CHead e (Bind b) u)
→flt e u (CHead c0 k t) (TLRef i)
we proved
∀e:C
.∀u:T
.∀i:nat.(getl i c (CHead e (Bind b) u))→(flt e u c (TLRef i))
we proved
∀b:B
.∀c:C
.∀e:C
.∀u:T
.∀i:nat.(getl i c (CHead e (Bind b) u))→(flt e u c (TLRef i))