DEFINITION arity_gen_cvoid_subst0()
TYPE =
∀g:G
.∀c:C
.∀t:T
.∀a:A
.arity g c t a
→∀d:C
.∀u:T
.∀i:nat
.getl i c (CHead d (Bind Void) u)
→∀w:T.∀v:T.(subst0 i w t v)→∀P:Prop.P
BODY =
assume g: G
assume c: C
assume t: T
assume a: A
suppose H: arity g c t a
we proceed by induction on H to prove
∀d:C
.∀u:T
.∀i:nat
.getl i c (CHead d (Bind Void) u)
→∀w:T.∀v:T.(subst0 i w t v)→∀P:Prop.P
case arity_sort : c0:C n:nat ⇒
the thesis becomes
∀d:C
.∀u:T
.∀i:nat
.getl i c0 (CHead d (Bind Void) u)
→∀w:T.∀v:T.∀H1:(subst0 i w (TSort n) v).∀P:Prop.P
assume d: C
assume u: T
assume i: nat
suppose : getl i c0 (CHead d (Bind Void) u)
assume w: T
assume v: T
suppose H1: subst0 i w (TSort n) v
assume P: Prop
by (subst0_gen_sort . . . . H1 .)
we proved P
∀d:C
.∀u:T
.∀i:nat
.getl i c0 (CHead d (Bind Void) u)
→∀w:T.∀v:T.∀H1:(subst0 i w (TSort n) v).∀P:Prop.P
case arity_abbr : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) a0:A :arity g d u a0 ⇒
the thesis becomes
∀d0:C.∀u0:T.∀i0:nat.∀H3:(getl i0 c0 (CHead d0 (Bind Void) u0)).∀w:T.∀v:T.∀H4:(subst0 i0 w (TLRef i) v).∀P:Prop.P
() by induction hypothesis we know
∀d0:C
.∀u0:T
.∀i0:nat
.(getl i0 d (CHead d0 (Bind Void) u0))→∀w:T.∀v:T.(subst0 i0 w u v)→∀P:Prop.P
assume d0: C
assume u0: T
assume i0: nat
suppose H3: getl i0 c0 (CHead d0 (Bind Void) u0)
assume w: T
assume v: T
suppose H4: subst0 i0 w (TLRef i) v
assume P: Prop
by (subst0_gen_lref . . . . H4)
we proved land (eq nat i i0) (eq T v (lift (S i) O w))
we proceed by induction on the previous result to prove P
case conj : H5:eq nat i i0 :eq T v (lift (S i) O w) ⇒
the thesis becomes P
(H7)
by (eq_ind_r . . . H3 . H5)
getl i c0 (CHead d0 (Bind Void) u0)
end of H7
(H9)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abbr) u) (CHead d0 (Bind Void) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead d0 (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abbr) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abbr) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead d0 (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
end of H9
consider H9
we proved
<λ:C.Prop>
CASE CHead d0 (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
P
we proved P
∀d0:C.∀u0:T.∀i0:nat.∀H3:(getl i0 c0 (CHead d0 (Bind Void) u0)).∀w:T.∀v:T.∀H4:(subst0 i0 w (TLRef i) v).∀P:Prop.P
case arity_abst : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abst) u) a0:A :arity g d u (asucc g a0) ⇒
the thesis becomes
∀d0:C.∀u0:T.∀i0:nat.∀H3:(getl i0 c0 (CHead d0 (Bind Void) u0)).∀w:T.∀v:T.∀H4:(subst0 i0 w (TLRef i) v).∀P:Prop.P
() by induction hypothesis we know
∀d0:C
.∀u0:T
.∀i0:nat
.(getl i0 d (CHead d0 (Bind Void) u0))→∀w:T.∀v:T.(subst0 i0 w u v)→∀P:Prop.P
assume d0: C
assume u0: T
assume i0: nat
suppose H3: getl i0 c0 (CHead d0 (Bind Void) u0)
assume w: T
assume v: T
suppose H4: subst0 i0 w (TLRef i) v
assume P: Prop
by (subst0_gen_lref . . . . H4)
we proved land (eq nat i i0) (eq T v (lift (S i) O w))
we proceed by induction on the previous result to prove P
case conj : H5:eq nat i i0 :eq T v (lift (S i) O w) ⇒
the thesis becomes P
(H7)
by (eq_ind_r . . . H3 . H5)
getl i c0 (CHead d0 (Bind Void) u0)
end of H7
(H9)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abst) u) (CHead d0 (Bind Void) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead d0 (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead d0 (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H9
consider H9
we proved
<λ:C.Prop>
CASE CHead d0 (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
P
we proved P
∀d0:C.∀u0:T.∀i0:nat.∀H3:(getl i0 c0 (CHead d0 (Bind Void) u0)).∀w:T.∀v:T.∀H4:(subst0 i0 w (TLRef i) v).∀P:Prop.P
case arity_bind : b:B :not (eq B b Abst) c0:C u:T a1:A :arity g c0 u a1 t0:T a2:A :arity g (CHead c0 (Bind b) u) t0 a2 ⇒
the thesis becomes
∀d:C
.∀u0:T
.∀i:nat
.∀H5:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H6:(subst0 i w (THead (Bind b) u t0) v).∀P:Prop.P
(H2) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.(getl i c0 (CHead d (Bind Void) u0))→∀w:T.∀v:T.(subst0 i w u v)→∀P:Prop.P
(H4) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.getl i (CHead c0 (Bind b) u) (CHead d (Bind Void) u0)
→∀w:T.∀v:T.(subst0 i w t0 v)→∀P:Prop.P
assume d: C
assume u0: T
assume i: nat
suppose H5: getl i c0 (CHead d (Bind Void) u0)
assume w: T
assume v: T
suppose H6: subst0 i w (THead (Bind b) u t0) v
assume P: Prop
by (subst0_gen_head . . . . . . H6)
we proved
or3
ex2 T λu2:T.eq T v (THead (Bind b) u2 t0) λu2:T.subst0 i w u u2
ex2 T λt2:T.eq T v (THead (Bind b) u t2) λt2:T.subst0 (s (Bind b) i) w t0 t2
ex3_2
T
T
λu2:T.λt2:T.eq T v (THead (Bind b) u2 t2)
λu2:T.λ:T.subst0 i w u u2
λ:T.λt2:T.subst0 (s (Bind b) i) w t0 t2
we proceed by induction on the previous result to prove P
case or3_intro0 : H7:ex2 T λu2:T.eq T v (THead (Bind b) u2 t0) λu2:T.subst0 i w u u2 ⇒
the thesis becomes P
we proceed by induction on H7 to prove P
case ex_intro2 : x:T :eq T v (THead (Bind b) x t0) H9:subst0 i w u x ⇒
the thesis becomes P
by (H2 . . . H5 . . H9 .)
P
P
case or3_intro1 : H7:ex2 T λt2:T.eq T v (THead (Bind b) u t2) λt2:T.subst0 (s (Bind b) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H7 to prove P
case ex_intro2 : x:T :eq T v (THead (Bind b) u x) H9:subst0 (s (Bind b) i) w t0 x ⇒
the thesis becomes P
(h1)
by (clear_bind . . .)
we proved clear (CHead c0 (Bind b) u) (CHead c0 (Bind b) u)
by (getl_clear_bind . . . . previous . . H5)
getl (S i) (CHead c0 (Bind b) u) (CHead d (Bind Void) u0)
end of h1
(h2)
consider H9
we proved subst0 (s (Bind b) i) w t0 x
subst0 (S i) w t0 x
end of h2
by (H4 . . . h1 . . h2 .)
P
P
case or3_intro2 : H7:ex3_2 T T λu2:T.λt2:T.eq T v (THead (Bind b) u2 t2) λu2:T.λ:T.subst0 i w u u2 λ:T.λt2:T.subst0 (s (Bind b) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H7 to prove P
case ex3_2_intro : x0:T x1:T :eq T v (THead (Bind b) x0 x1) H9:subst0 i w u x0 :subst0 (s (Bind b) i) w t0 x1 ⇒
the thesis becomes P
by (H2 . . . H5 . . H9 .)
P
P
we proved P
∀d:C
.∀u0:T
.∀i:nat
.∀H5:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H6:(subst0 i w (THead (Bind b) u t0) v).∀P:Prop.P
case arity_head : c0:C u:T a1:A :arity g c0 u (asucc g a1) t0:T a2:A :arity g (CHead c0 (Bind Abst) u) t0 a2 ⇒
the thesis becomes
∀d:C
.∀u0:T
.∀i:nat
.∀H4:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H5:(subst0 i w (THead (Bind Abst) u t0) v).∀P:Prop.P
(H1) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.(getl i c0 (CHead d (Bind Void) u0))→∀w:T.∀v:T.(subst0 i w u v)→∀P:Prop.P
(H3) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.getl i (CHead c0 (Bind Abst) u) (CHead d (Bind Void) u0)
→∀w:T.∀v:T.(subst0 i w t0 v)→∀P:Prop.P
assume d: C
assume u0: T
assume i: nat
suppose H4: getl i c0 (CHead d (Bind Void) u0)
assume w: T
assume v: T
suppose H5: subst0 i w (THead (Bind Abst) u t0) v
assume P: Prop
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T v (THead (Bind Abst) u2 t0) λu2:T.subst0 i w u u2
ex2 T λt2:T.eq T v (THead (Bind Abst) u t2) λt2:T.subst0 (s (Bind Abst) i) w t0 t2
ex3_2
T
T
λu2:T.λt2:T.eq T v (THead (Bind Abst) u2 t2)
λu2:T.λ:T.subst0 i w u u2
λ:T.λt2:T.subst0 (s (Bind Abst) i) w t0 t2
we proceed by induction on the previous result to prove P
case or3_intro0 : H6:ex2 T λu2:T.eq T v (THead (Bind Abst) u2 t0) λu2:T.subst0 i w u u2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex_intro2 : x:T :eq T v (THead (Bind Abst) x t0) H8:subst0 i w u x ⇒
the thesis becomes P
by (H1 . . . H4 . . H8 .)
P
P
case or3_intro1 : H6:ex2 T λt2:T.eq T v (THead (Bind Abst) u t2) λt2:T.subst0 (s (Bind Abst) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex_intro2 : x:T :eq T v (THead (Bind Abst) u x) H8:subst0 (s (Bind Abst) i) w t0 x ⇒
the thesis becomes P
(h1)
by (clear_bind . . .)
we proved clear (CHead c0 (Bind Abst) u) (CHead c0 (Bind Abst) u)
by (getl_clear_bind . . . . previous . . H4)
getl (S i) (CHead c0 (Bind Abst) u) (CHead d (Bind Void) u0)
end of h1
(h2)
consider H8
we proved subst0 (s (Bind Abst) i) w t0 x
subst0 (S i) w t0 x
end of h2
by (H3 . . . h1 . . h2 .)
P
P
case or3_intro2 : H6:ex3_2 T T λu2:T.λt2:T.eq T v (THead (Bind Abst) u2 t2) λu2:T.λ:T.subst0 i w u u2 λ:T.λt2:T.subst0 (s (Bind Abst) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex3_2_intro : x0:T x1:T :eq T v (THead (Bind Abst) x0 x1) H8:subst0 i w u x0 :subst0 (s (Bind Abst) i) w t0 x1 ⇒
the thesis becomes P
by (H1 . . . H4 . . H8 .)
P
P
we proved P
∀d:C
.∀u0:T
.∀i:nat
.∀H4:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H5:(subst0 i w (THead (Bind Abst) u t0) v).∀P:Prop.P
case arity_appl : c0:C u:T a1:A :arity g c0 u a1 t0:T a2:A :arity g c0 t0 (AHead a1 a2) ⇒
the thesis becomes
∀d:C
.∀u0:T
.∀i:nat
.∀H4:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H5:(subst0 i w (THead (Flat Appl) u t0) v).∀P:Prop.P
(H1) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.(getl i c0 (CHead d (Bind Void) u0))→∀w:T.∀v:T.(subst0 i w u v)→∀P:Prop.P
(H3) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.(getl i c0 (CHead d (Bind Void) u0))→∀w:T.∀v:T.(subst0 i w t0 v)→∀P:Prop.P
assume d: C
assume u0: T
assume i: nat
suppose H4: getl i c0 (CHead d (Bind Void) u0)
assume w: T
assume v: T
suppose H5: subst0 i w (THead (Flat Appl) u t0) v
assume P: Prop
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T v (THead (Flat Appl) u2 t0) λu2:T.subst0 i w u u2
ex2 T λt2:T.eq T v (THead (Flat Appl) u t2) λt2:T.subst0 (s (Flat Appl) i) w t0 t2
ex3_2
T
T
λu2:T.λt2:T.eq T v (THead (Flat Appl) u2 t2)
λu2:T.λ:T.subst0 i w u u2
λ:T.λt2:T.subst0 (s (Flat Appl) i) w t0 t2
we proceed by induction on the previous result to prove P
case or3_intro0 : H6:ex2 T λu2:T.eq T v (THead (Flat Appl) u2 t0) λu2:T.subst0 i w u u2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex_intro2 : x:T :eq T v (THead (Flat Appl) x t0) H8:subst0 i w u x ⇒
the thesis becomes P
by (H1 . . . H4 . . H8 .)
P
P
case or3_intro1 : H6:ex2 T λt2:T.eq T v (THead (Flat Appl) u t2) λt2:T.subst0 (s (Flat Appl) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex_intro2 : x:T :eq T v (THead (Flat Appl) u x) H8:subst0 (s (Flat Appl) i) w t0 x ⇒
the thesis becomes P
consider H8
we proved subst0 (s (Flat Appl) i) w t0 x
that is equivalent to subst0 i w t0 x
by (H3 . . . H4 . . previous .)
P
P
case or3_intro2 : H6:ex3_2 T T λu2:T.λt2:T.eq T v (THead (Flat Appl) u2 t2) λu2:T.λ:T.subst0 i w u u2 λ:T.λt2:T.subst0 (s (Flat Appl) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex3_2_intro : x0:T x1:T :eq T v (THead (Flat Appl) x0 x1) H8:subst0 i w u x0 :subst0 (s (Flat Appl) i) w t0 x1 ⇒
the thesis becomes P
by (H1 . . . H4 . . H8 .)
P
P
we proved P
∀d:C
.∀u0:T
.∀i:nat
.∀H4:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H5:(subst0 i w (THead (Flat Appl) u t0) v).∀P:Prop.P
case arity_cast : c0:C u:T a0:A :arity g c0 u (asucc g a0) t0:T :arity g c0 t0 a0 ⇒
the thesis becomes
∀d:C
.∀u0:T
.∀i:nat
.∀H4:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H5:(subst0 i w (THead (Flat Cast) u t0) v).∀P:Prop.P
(H1) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.(getl i c0 (CHead d (Bind Void) u0))→∀w:T.∀v:T.(subst0 i w u v)→∀P:Prop.P
(H3) by induction hypothesis we know
∀d:C
.∀u0:T
.∀i:nat
.(getl i c0 (CHead d (Bind Void) u0))→∀w:T.∀v:T.(subst0 i w t0 v)→∀P:Prop.P
assume d: C
assume u0: T
assume i: nat
suppose H4: getl i c0 (CHead d (Bind Void) u0)
assume w: T
assume v: T
suppose H5: subst0 i w (THead (Flat Cast) u t0) v
assume P: Prop
by (subst0_gen_head . . . . . . H5)
we proved
or3
ex2 T λu2:T.eq T v (THead (Flat Cast) u2 t0) λu2:T.subst0 i w u u2
ex2 T λt2:T.eq T v (THead (Flat Cast) u t2) λt2:T.subst0 (s (Flat Cast) i) w t0 t2
ex3_2
T
T
λu2:T.λt2:T.eq T v (THead (Flat Cast) u2 t2)
λu2:T.λ:T.subst0 i w u u2
λ:T.λt2:T.subst0 (s (Flat Cast) i) w t0 t2
we proceed by induction on the previous result to prove P
case or3_intro0 : H6:ex2 T λu2:T.eq T v (THead (Flat Cast) u2 t0) λu2:T.subst0 i w u u2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex_intro2 : x:T :eq T v (THead (Flat Cast) x t0) H8:subst0 i w u x ⇒
the thesis becomes P
by (H1 . . . H4 . . H8 .)
P
P
case or3_intro1 : H6:ex2 T λt2:T.eq T v (THead (Flat Cast) u t2) λt2:T.subst0 (s (Flat Cast) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex_intro2 : x:T :eq T v (THead (Flat Cast) u x) H8:subst0 (s (Flat Cast) i) w t0 x ⇒
the thesis becomes P
consider H8
we proved subst0 (s (Flat Cast) i) w t0 x
that is equivalent to subst0 i w t0 x
by (H3 . . . H4 . . previous .)
P
P
case or3_intro2 : H6:ex3_2 T T λu2:T.λt2:T.eq T v (THead (Flat Cast) u2 t2) λu2:T.λ:T.subst0 i w u u2 λ:T.λt2:T.subst0 (s (Flat Cast) i) w t0 t2 ⇒
the thesis becomes P
we proceed by induction on H6 to prove P
case ex3_2_intro : x0:T x1:T :eq T v (THead (Flat Cast) x0 x1) H8:subst0 i w u x0 :subst0 (s (Flat Cast) i) w t0 x1 ⇒
the thesis becomes P
by (H1 . . . H4 . . H8 .)
P
P
we proved P
∀d:C
.∀u0:T
.∀i:nat
.∀H4:getl i c0 (CHead d (Bind Void) u0)
.∀w:T.∀v:T.∀H5:(subst0 i w (THead (Flat Cast) u t0) v).∀P:Prop.P
case arity_repl : c0:C t0:T a1:A :arity g c0 t0 a1 a2:A :leq g a1 a2 ⇒
the thesis becomes ∀d:C.∀u:T.∀i:nat.∀H3:(getl i c0 (CHead d (Bind Void) u)).∀w:T.∀v:T.∀H4:(subst0 i w t0 v).∀P:Prop.P
(H1) by induction hypothesis we know
∀d:C
.∀u:T
.∀i:nat
.(getl i c0 (CHead d (Bind Void) u))→∀w:T.∀v:T.(subst0 i w t0 v)→∀P:Prop.P
assume d: C
assume u: T
assume i: nat
suppose H3: getl i c0 (CHead d (Bind Void) u)
assume w: T
assume v: T
suppose H4: subst0 i w t0 v
assume P: Prop
by (H1 . . . H3 . . H4 .)
we proved P
∀d:C.∀u:T.∀i:nat.∀H3:(getl i c0 (CHead d (Bind Void) u)).∀w:T.∀v:T.∀H4:(subst0 i w t0 v).∀P:Prop.P
we proved
∀d:C
.∀u:T
.∀i:nat
.getl i c (CHead d (Bind Void) u)
→∀w:T.∀v:T.(subst0 i w t v)→∀P:Prop.P
we proved
∀g:G
.∀c:C
.∀t:T
.∀a:A
.arity g c t a
→∀d:C
.∀u:T
.∀i:nat
.getl i c (CHead d (Bind Void) u)
→∀w:T.∀v:T.(subst0 i w t v)→∀P:Prop.P