DEFINITION arity_gen_lref()
TYPE =
∀g:G
.∀c:C
.∀i:nat
.∀a:A
.arity g c (TLRef i) a
→(or
ex2_2 C T λd:C.λu:T.getl i c (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a))
BODY =
assume g: G
assume c: C
assume i: nat
assume a: A
suppose H: arity g c (TLRef i) a
assume y: T
suppose H0: arity g c y a
we proceed by induction on H0 to prove
eq T y (TLRef i)
→(or
ex2_2 C T λd:C.λu:T.getl i c (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a))
case arity_sort : c0:C n:nat ⇒
the thesis becomes
∀H1:eq T (TSort n) (TLRef i)
.or
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u)
λd:C.λu:T.arity g d u (ASort O n)
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g (ASort O n))
suppose H1: eq T (TSort n) (TLRef i)
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u)
λd:C.λu:T.arity g d u (ASort O n)
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g (ASort O n))
we proved
or
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u)
λd:C.λu:T.arity g d u (ASort O n)
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g (ASort O n))
∀H1:eq T (TSort n) (TLRef i)
.or
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u)
λd:C.λu:T.arity g d u (ASort O n)
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g (ASort O n))
case arity_abbr : c0:C d:C u:T i0:nat H1:getl i0 c0 (CHead d (Bind Abbr) u) a0:A H2:arity g d u a0 ⇒
the thesis becomes
∀H4:eq T (TLRef i0) (TLRef i)
.or
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
() by induction hypothesis we know
eq T u (TLRef i)
→(or
ex2_2 C T λd0:C.λu0:T.getl i d (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
ex2_2 C T λd0:C.λu0:T.getl i d (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0))
suppose H4: eq T (TLRef i0) (TLRef i)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef i0 OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
<λ:T.nat> CASE TLRef i OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0 (TLRef i0)
λe:T.<λ:T.nat> CASE e OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0 (TLRef i)
end of H5
(H6)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef i0 OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
<λ:T.nat> CASE TLRef i OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
that is equivalent to eq nat i0 i
we proceed by induction on the previous result to prove getl i c0 (CHead d (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl i c0 (CHead d (Bind Abbr) u)
end of H6
by (ex2_2_intro . . . . . . H6 H2)
we proved ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
by (or_introl . . previous)
we proved
or
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
∀H4:eq T (TLRef i0) (TLRef i)
.or
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
case arity_abst : c0:C d:C u:T i0:nat H1:getl i0 c0 (CHead d (Bind Abst) u) a0:A H2:arity g d u (asucc g a0) ⇒
the thesis becomes
∀H4:eq T (TLRef i0) (TLRef i)
.or
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
() by induction hypothesis we know
eq T u (TLRef i)
→(or
ex2_2 C T λd0:C.λu0:T.getl i d (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
ex2_2
C
T
λd0:C.λu0:T.getl i d (CHead d0 (Bind Abst) u0)
λd0:C.λu0:T.arity g d0 u0 (asucc g (asucc g a0)))
suppose H4: eq T (TLRef i0) (TLRef i)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:T.nat> CASE TLRef i0 OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
<λ:T.nat> CASE TLRef i OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0 (TLRef i0)
λe:T.<λ:T.nat> CASE e OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0 (TLRef i)
end of H5
(H6)
consider H5
we proved
eq
nat
<λ:T.nat> CASE TLRef i0 OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
<λ:T.nat> CASE TLRef i OF TSort ⇒i0 | TLRef n⇒n | THead ⇒i0
that is equivalent to eq nat i0 i
we proceed by induction on the previous result to prove getl i c0 (CHead d (Bind Abst) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
getl i c0 (CHead d (Bind Abst) u)
end of H6
by (ex2_2_intro . . . . . . H6 H2)
we proved ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
by (or_intror . . previous)
we proved
or
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
∀H4:eq T (TLRef i0) (TLRef i)
.or
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abbr) u0) λd0:C.λu0:T.arity g d0 u0 a0
ex2_2 C T λd0:C.λu0:T.getl i c0 (CHead d0 (Bind Abst) u0) λd0:C.λu0:T.arity g d0 u0 (asucc g a0)
case arity_bind : b:B :not (eq B b Abst) c0:C u:T a1:A :arity g c0 u a1 t:T a2:A :arity g (CHead c0 (Bind b) u) t a2 ⇒
the thesis becomes
∀H6:eq T (THead (Bind b) u t) (TLRef i)
.or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
() by induction hypothesis we know
eq T u (TLRef i)
→(or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a1
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a1))
() by induction hypothesis we know
eq T t (TLRef i)
→(or
ex2_2
C
T
λd:C.λu0:T.getl i (CHead c0 (Bind b) u) (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i (CHead c0 (Bind b) u) (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2))
suppose H6: eq T (THead (Bind b) u t) (TLRef i)
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H7
consider H7
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
we proved
or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
∀H6:eq T (THead (Bind b) u t) (TLRef i)
.or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
case arity_head : c0:C u:T a1:A :arity g c0 u (asucc g a1) t:T a2:A :arity g (CHead c0 (Bind Abst) u) t a2 ⇒
the thesis becomes
∀H5:eq T (THead (Bind Abst) u t) (TLRef i)
.or
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 (AHead a1 a2)
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g (AHead a1 a2))
() by induction hypothesis we know
eq T u (TLRef i)
→(or
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 (asucc g a1)
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g (asucc g a1)))
() by induction hypothesis we know
eq T t (TLRef i)
→(or
ex2_2
C
T
λd:C.λu0:T.getl i (CHead c0 (Bind Abst) u) (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i (CHead c0 (Bind Abst) u) (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2))
suppose H5: eq T (THead (Bind Abst) u t) (TLRef i)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 (AHead a1 a2)
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g (AHead a1 a2))
we proved
or
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 (AHead a1 a2)
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g (AHead a1 a2))
∀H5:eq T (THead (Bind Abst) u t) (TLRef i)
.or
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 (AHead a1 a2)
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g (AHead a1 a2))
case arity_appl : c0:C u:T a1:A :arity g c0 u a1 t:T a2:A :arity g c0 t (AHead a1 a2) ⇒
the thesis becomes
∀H5:eq T (THead (Flat Appl) u t) (TLRef i)
.or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
() by induction hypothesis we know
eq T u (TLRef i)
→(or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a1
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a1))
() by induction hypothesis we know
eq T t (TLRef i)
→(or
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 (AHead a1 a2)
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g (AHead a1 a2)))
suppose H5: eq T (THead (Flat Appl) u t) (TLRef i)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
we proved
or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
∀H5:eq T (THead (Flat Appl) u t) (TLRef i)
.or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a2
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a2)
case arity_cast : c0:C u:T a0:A :arity g c0 u (asucc g a0) t:T :arity g c0 t a0 ⇒
the thesis becomes
∀H5:eq T (THead (Flat Cast) u t) (TLRef i)
.or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a0
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a0)
() by induction hypothesis we know
eq T u (TLRef i)
→(or
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0)
λd:C.λu0:T.arity g d u0 (asucc g a0)
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g (asucc g a0)))
() by induction hypothesis we know
eq T t (TLRef i)
→(or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a0
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a0))
suppose H5: eq T (THead (Flat Cast) u t) (TLRef i)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a0
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a0)
we proved
or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a0
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a0)
∀H5:eq T (THead (Flat Cast) u t) (TLRef i)
.or
ex2_2 C T λd:C.λu0:T.getl i c0 (CHead d (Bind Abbr) u0) λd:C.λu0:T.arity g d u0 a0
ex2_2
C
T
λd:C.λu0:T.getl i c0 (CHead d (Bind Abst) u0)
λd:C.λu0:T.arity g d u0 (asucc g a0)
case arity_repl : c0:C t:T a1:A H1:arity g c0 t a1 a2:A H3:leq g a1 a2 ⇒
the thesis becomes
∀H4:eq T t (TLRef i)
.or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
(H2) by induction hypothesis we know
eq T t (TLRef i)
→(or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a1
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a1))
suppose H4: eq T t (TLRef i)
(H5)
by (f_equal . . . . . H4)
we proved eq T t (TLRef i)
eq T (λe:T.e t) (λe:T.e (TLRef i))
end of H5
(H6)
we proceed by induction on H5 to prove
eq T (TLRef i) (TLRef i)
→(or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a1
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a1))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq T (TLRef i) (TLRef i)
→(or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a1
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a1))
end of H6
(H8)
by (refl_equal . .)
we proved eq T (TLRef i) (TLRef i)
by (H6 previous)
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a1
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a1)
end of H8
we proceed by induction on H8 to prove
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
case or_introl : H9:ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a1 ⇒
the thesis becomes
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
we proceed by induction on H9 to prove
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
case ex2_2_intro : x0:C x1:T H10:getl i c0 (CHead x0 (Bind Abbr) x1) H11:arity g x0 x1 a1 ⇒
the thesis becomes
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
by (arity_repl . . . . H11 . H3)
we proved arity g x0 x1 a2
by (ex2_2_intro . . . . . . H10 previous)
we proved ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
by (or_introl . . previous)
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
case or_intror : H9:ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u) λd:C.λu:T.arity g d u (asucc g a1) ⇒
the thesis becomes
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
we proceed by induction on H9 to prove
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
case ex2_2_intro : x0:C x1:T H10:getl i c0 (CHead x0 (Bind Abst) x1) H11:arity g x0 x1 (asucc g a1) ⇒
the thesis becomes
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
by (asucc_repl . . . H3)
we proved leq g (asucc g a1) (asucc g a2)
by (arity_repl . . . . H11 . previous)
we proved arity g x0 x1 (asucc g a2)
by (ex2_2_intro . . . . . . H10 previous)
we proved
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
by (or_intror . . previous)
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
we proved
or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
∀H4:eq T t (TLRef i)
.or
ex2_2 C T λd:C.λu:T.getl i c0 (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a2
ex2_2
C
T
λd:C.λu:T.getl i c0 (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a2)
we proved
eq T y (TLRef i)
→(or
ex2_2 C T λd:C.λu:T.getl i c (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a))
we proved
∀y:T
.arity g c y a
→(eq T y (TLRef i)
→(or
ex2_2 C T λd:C.λu:T.getl i c (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a)))
by (insert_eq . . . . previous H)
we proved
or
ex2_2 C T λd:C.λu:T.getl i c (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a)
we proved
∀g:G
.∀c:C
.∀i:nat
.∀a:A
.arity g c (TLRef i) a
→(or
ex2_2 C T λd:C.λu:T.getl i c (CHead d (Bind Abbr) u) λd:C.λu:T.arity g d u a
ex2_2
C
T
λd:C.λu:T.getl i c (CHead d (Bind Abst) u)
λd:C.λu:T.arity g d u (asucc g a))