DEFINITION getl_dec()
TYPE =
∀c:C
.∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i c (CHead e (Bind b) v)
∀d:C.(getl i c d)→∀P:Prop.P
BODY =
assume c: C
we proceed by induction on c to prove
∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i c (CHead e (Bind b) v)
∀d:C.(getl i c d)→∀P:Prop.P
case CSort : n:nat ⇒
the thesis becomes
∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i (CSort n) (CHead e (Bind b) v)
∀d:C.(getl i (CSort n) d)→∀P:Prop.P
assume i: nat
assume d: C
suppose H: getl i (CSort n) d
assume P: Prop
by (getl_gen_sort . . . H .)
we proved P
we proved ∀d:C.(getl i (CSort n) d)→∀P:Prop.P
by (or_intror . . previous)
we proved
or
ex_3 C B T λe:C.λb:B.λv:T.getl i (CSort n) (CHead e (Bind b) v)
∀d:C.(getl i (CSort n) d)→∀P:Prop.P
∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i (CSort n) (CHead e (Bind b) v)
∀d:C.(getl i (CSort n) d)→∀P:Prop.P
case CHead : c0:C k:K t:T ⇒
the thesis becomes
∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl i (CHead c0 k t) d)→∀P:Prop.P
(H) by induction hypothesis we know
∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i c0 (CHead e (Bind b) v)
∀d:C.(getl i c0 d)→∀P:Prop.P
assume i: nat
we proceed by induction on i to prove
or
ex_3 C B T λe:C.λb:B.λv:T.getl i (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl i (CHead c0 k t) d)→∀P:Prop.P
case O : ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 k t) d)→∀P:Prop.P
we proceed by induction on k to prove
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 k t) d)→∀P:Prop.P
case Bind : b:B ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb0:B.λv:T.getl O (CHead c0 (Bind b) t) (CHead e (Bind b0) v)
∀d:C.(getl O (CHead c0 (Bind b) t) d)→∀P:Prop.P
by (getl_refl . . .)
we proved getl O (CHead c0 (Bind b) t) (CHead c0 (Bind b) t)
by (ex_3_intro . . . . . . . previous)
we proved ex_3 C B T λe:C.λb0:B.λv:T.getl O (CHead c0 (Bind b) t) (CHead e (Bind b0) v)
by (or_introl . . previous)
or
ex_3 C B T λe:C.λb0:B.λv:T.getl O (CHead c0 (Bind b) t) (CHead e (Bind b0) v)
∀d:C.(getl O (CHead c0 (Bind b) t) d)→∀P:Prop.P
case Flat : f:F ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
(H_x)
by (H .)
or
ex_3 C B T λe:C.λb:B.λv:T.getl O c0 (CHead e (Bind b) v)
∀d:C.(getl O c0 d)→∀P:Prop.P
end of H_x
(H0) consider H_x
we proceed by induction on H0 to prove
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
case or_introl : H1:ex_3 C B T λe:C.λb:B.λv:T.getl O c0 (CHead e (Bind b) v) ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
we proceed by induction on H1 to prove
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
case ex_3_intro : x0:C x1:B x2:T H2:getl O c0 (CHead x0 (Bind x1) x2) ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
by (getl_flat . . . H2 . .)
we proved getl O (CHead c0 (Flat f) t) (CHead x0 (Bind x1) x2)
by (ex_3_intro . . . . . . . previous)
we proved
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
by (or_introl . . previous)
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
case or_intror : H1:∀d:C.(getl O c0 d)→∀P:Prop.P ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
assume d: C
suppose H2: getl O (CHead c0 (Flat f) t) d
assume P: Prop
(h1)
by (drop_refl .)
drop O O c0 c0
end of h1
(h2)
by (getl_gen_O . . H2)
we proved clear (CHead c0 (Flat f) t) d
by (clear_gen_flat . . . . previous)
clear c0 d
end of h2
by (getl_intro . . . . h1 h2)
we proved getl O c0 d
by (H1 . previous .)
we proved P
we proved ∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
by (or_intror . . previous)
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 (Flat f) t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 (Flat f) t) d)→∀P:Prop.P
or
ex_3 C B T λe:C.λb:B.λv:T.getl O (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl O (CHead c0 k t) d)→∀P:Prop.P
case S : n:nat ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
() by induction hypothesis we know
or
ex_3 C B T λe:C.λb:B.λv:T.getl n (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl n (CHead c0 k t) d)→∀P:Prop.P
(H_x)
by (H .)
or
ex_3 C B T λe:C.λb:B.λv:T.getl (r k n) c0 (CHead e (Bind b) v)
∀d:C.(getl (r k n) c0 d)→∀P:Prop.P
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
case or_introl : H2:ex_3 C B T λe:C.λb:B.λv:T.getl (r k n) c0 (CHead e (Bind b) v) ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
we proceed by induction on H2 to prove
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
case ex_3_intro : x0:C x1:B x2:T H3:getl (r k n) c0 (CHead x0 (Bind x1) x2) ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
by (getl_head . . . . H3 .)
we proved getl (S n) (CHead c0 k t) (CHead x0 (Bind x1) x2)
by (ex_3_intro . . . . . . . previous)
we proved ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
by (or_introl . . previous)
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
case or_intror : H2:∀d:C.(getl (r k n) c0 d)→∀P:Prop.P ⇒
the thesis becomes
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
assume d: C
suppose H3: getl (S n) (CHead c0 k t) d
assume P: Prop
by (getl_gen_S . . . . . H3)
we proved getl (r k n) c0 d
by (H2 . previous .)
we proved P
we proved ∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
by (or_intror . . previous)
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
or
ex_3 C B T λe:C.λb:B.λv:T.getl (S n) (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl (S n) (CHead c0 k t) d)→∀P:Prop.P
we proved
or
ex_3 C B T λe:C.λb:B.λv:T.getl i (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl i (CHead c0 k t) d)→∀P:Prop.P
∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i (CHead c0 k t) (CHead e (Bind b) v)
∀d:C.(getl i (CHead c0 k t) d)→∀P:Prop.P
we proved
∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i c (CHead e (Bind b) v)
∀d:C.(getl i c d)→∀P:Prop.P
we proved
∀c:C
.∀i:nat
.or
ex_3 C B T λe:C.λb:B.λv:T.getl i c (CHead e (Bind b) v)
∀d:C.(getl i c d)→∀P:Prop.P