DEFINITION abst_dec()
TYPE =
∀u:T
.∀v:T
.or
ex T λt:T.eq T u (THead (Bind Abst) v t)
∀t:T.(eq T u (THead (Bind Abst) v t))→∀P:Prop.P
BODY =
assume u: T
we proceed by induction on u to prove
∀v:T
.or
ex T λt0:T.eq T u (THead (Bind Abst) v t0)
∀t0:T.(eq T u (THead (Bind Abst) v t0))→∀P:Prop.P
case TSort : n:nat ⇒
the thesis becomes
∀v:T
.or
ex T λt:T.eq T (TSort n) (THead (Bind Abst) v t)
∀t:T.(eq T (TSort n) (THead (Bind Abst) v t))→∀P:Prop.P
assume v: T
assume t: T
suppose H: eq T (TSort n) (THead (Bind Abst) v t)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE THead (Bind Abst) v t 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 THead (Bind Abst) v t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H0
consider H0
we proved
<λ:T.Prop>
CASE THead (Bind Abst) v t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved ∀t:T.(eq T (TSort n) (THead (Bind Abst) v t))→∀P:Prop.P
by (or_intror . . previous)
we proved
or
ex T λt:T.eq T (TSort n) (THead (Bind Abst) v t)
∀t:T.(eq T (TSort n) (THead (Bind Abst) v t))→∀P:Prop.P
∀v:T
.or
ex T λt:T.eq T (TSort n) (THead (Bind Abst) v t)
∀t:T.(eq T (TSort n) (THead (Bind Abst) v t))→∀P:Prop.P
case TLRef : n:nat ⇒
the thesis becomes
∀v:T
.or
ex T λt:T.eq T (TLRef n) (THead (Bind Abst) v t)
∀t:T.(eq T (TLRef n) (THead (Bind Abst) v t))→∀P:Prop.P
assume v: T
assume t: T
suppose H: eq T (TLRef n) (THead (Bind Abst) v t)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE THead (Bind Abst) v t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) v t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H0
consider H0
we proved
<λ:T.Prop>
CASE THead (Bind Abst) v t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved ∀t:T.(eq T (TLRef n) (THead (Bind Abst) v t))→∀P:Prop.P
by (or_intror . . previous)
we proved
or
ex T λt:T.eq T (TLRef n) (THead (Bind Abst) v t)
∀t:T.(eq T (TLRef n) (THead (Bind Abst) v t))→∀P:Prop.P
∀v:T
.or
ex T λt:T.eq T (TLRef n) (THead (Bind Abst) v t)
∀t:T.(eq T (TLRef n) (THead (Bind Abst) v t))→∀P:Prop.P
case THead : k:K t:T t0:T ⇒
the thesis becomes
∀v:T
.or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
() by induction hypothesis we know
∀v:T
.or
ex T λt0:T.eq T t (THead (Bind Abst) v t0)
∀t0:T.(eq T t (THead (Bind Abst) v t0))→∀P:Prop.P
() by induction hypothesis we know
∀v:T
.or
ex T λt1:T.eq T t0 (THead (Bind Abst) v t1)
∀t1:T.(eq T t0 (THead (Bind Abst) v t1))→∀P:Prop.P
assume v: T
(H_x)
by (terms_props__kind_dec . .)
or (eq K k (Bind Abst)) (eq K k (Bind Abst))→∀P:Prop.P
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
case or_introl : H2:eq K k (Bind Abst) ⇒
the thesis becomes
or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
(H_x0)
by (term_dec . .)
or (eq T t v) (eq T t v)→∀P:Prop.P
end of H_x0
(H3) consider H_x0
we proceed by induction on H3 to prove
or
ex T λt1:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
∀t1:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
→∀P:Prop.P
case or_introl : H4:eq T t v ⇒
the thesis becomes
or
ex T λt2:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t2)
∀t2:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t2)
→∀P:Prop.P
we proceed by induction on H4 to prove
or
ex T λt2:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t2)
∀t2:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t2)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes
or
ex T λt1:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1)
∀t1:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1)
→∀P:Prop.P
by (refl_equal . .)
we proved eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t0)
by (ex_intro . . . previous)
we proved ex T λt1:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1)
by (or_introl . . previous)
or
ex T λt1:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1)
∀t1:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) t t1)
→∀P:Prop.P
or
ex T λt2:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t2)
∀t2:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t2)
→∀P:Prop.P
case or_intror : H4:(eq T t v)→∀P:Prop.P ⇒
the thesis becomes
or
ex T λt1:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
∀t1:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
→∀P:Prop.P
assume t1: T
suppose H5: eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
assume P: Prop
(H6)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Abst) v t1 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Bind Abst) t t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Bind Abst) v t1
end of H6
(H8)
consider H6
we proved
eq
T
<λ:T.T> CASE THead (Bind Abst) t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Abst) v t1 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
eq T t v
end of H8
by (H4 H8 .)
we proved P
we proved
∀t1:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
→∀P:Prop.P
by (or_intror . . previous)
or
ex T λt1:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
∀t1:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
→∀P:Prop.P
we proved
or
ex T λt1:T.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
∀t1:T
.eq T (THead (Bind Abst) t t0) (THead (Bind Abst) v t1)
→∀P:Prop.P
by (eq_ind_r . . . previous . H2)
or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
case or_intror : H2:(eq K k (Bind Abst))→∀P:Prop.P ⇒
the thesis becomes
or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
assume t1: T
suppose H3: eq T (THead k t t0) (THead (Bind Abst) v t1)
assume P: Prop
(H4)
by (f_equal . . . . . H3)
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Bind Abst) v t1 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0 (THead k t t0)
λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
THead (Bind Abst) v t1
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Abst) v t1 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2 (THead k t t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
THead (Bind Abst) v t1
end of H5
()
consider H5
we proved
eq
T
<λ:T.T> CASE THead k t t0 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
<λ:T.T> CASE THead (Bind Abst) v t1 OF TSort ⇒t | TLRef ⇒t | THead t2 ⇒t2
eq T t v
end of
suppose H8: eq K k (Bind Abst)
by (H2 H8 .)
we proved P
(eq K k (Bind Abst))→P
end of h1
(h2)
consider H4
we proved
eq
K
<λ:T.K> CASE THead k t t0 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
<λ:T.K> CASE THead (Bind Abst) v t1 OF TSort ⇒k | TLRef ⇒k | THead k0 ⇒k0
eq K k (Bind Abst)
end of h2
by (h1 h2)
we proved P
we proved ∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
by (or_intror . . previous)
or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
we proved
or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
∀v:T
.or
ex T λt1:T.eq T (THead k t t0) (THead (Bind Abst) v t1)
∀t1:T.(eq T (THead k t t0) (THead (Bind Abst) v t1))→∀P:Prop.P
we proved
∀v:T
.or
ex T λt0:T.eq T u (THead (Bind Abst) v t0)
∀t0:T.(eq T u (THead (Bind Abst) v t0))→∀P:Prop.P
we proved
∀u:T
.∀v:T
.or
ex T λt0:T.eq T u (THead (Bind Abst) v t0)
∀t0:T.(eq T u (THead (Bind Abst) v t0))→∀P:Prop.P