DEFINITION binder_dec()
TYPE =
∀t:T
.or
ex_3 B T T λb:B.λw:T.λu:T.eq T t (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t (THead (Bind b) w u))→∀P:Prop.P
BODY =
assume t: T
we proceed by induction on t to prove
or
ex_3 B T T λb:B.λw:T.λu:T.eq T t (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t (THead (Bind b) w u))→∀P:Prop.P
case TSort : n:nat ⇒
the thesis becomes
or
ex_3 B T T λb:B.λw:T.λu:T.eq T (TSort n) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (TSort n) (THead (Bind b) w u))→∀P:Prop.P
assume b: B
assume w: T
assume u: T
suppose H: eq T (TSort n) (THead (Bind b) w u)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE THead (Bind b) w u 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 b) w u OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H0
consider H0
we proved
<λ:T.Prop>
CASE THead (Bind b) w u 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 ∀b:B.∀w:T.∀u:T.(eq T (TSort n) (THead (Bind b) w u))→∀P:Prop.P
by (or_intror . . previous)
or
ex_3 B T T λb:B.λw:T.λu:T.eq T (TSort n) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (TSort n) (THead (Bind b) w u))→∀P:Prop.P
case TLRef : n:nat ⇒
the thesis becomes
or
ex_3 B T T λb:B.λw:T.λu:T.eq T (TLRef n) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (TLRef n) (THead (Bind b) w u))→∀P:Prop.P
assume b: B
assume w: T
assume u: T
suppose H: eq T (TLRef n) (THead (Bind b) w u)
assume P: Prop
(H0)
we proceed by induction on H to prove
<λ:T.Prop>
CASE THead (Bind b) w u 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 b) w u OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H0
consider H0
we proved
<λ:T.Prop>
CASE THead (Bind b) w u 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 ∀b:B.∀w:T.∀u:T.(eq T (TLRef n) (THead (Bind b) w u))→∀P:Prop.P
by (or_intror . . previous)
or
ex_3 B T T λb:B.λw:T.λu:T.eq T (TLRef n) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (TLRef n) (THead (Bind b) w u))→∀P:Prop.P
case THead ⇒
we need to prove
∀k:K
.∀t0:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t1 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb:B.λw:T.λu:T.eq T (THead k t0 t1) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (THead k t0 t1) (THead (Bind b) w u))→∀P:Prop.P)
assume k: K
we proceed by induction on k to prove
∀t0:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t1 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb:B.λw:T.λu:T.eq T (THead k t0 t1) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (THead k t0 t1) (THead (Bind b) w u))→∀P:Prop.P)
case Bind : b:B ⇒
the thesis becomes
∀t0:T
.(or
ex_3 B T T λb0:B.λw:T.λu:T.eq T t0 (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b0) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb0:B.λw:T.λu:T.eq T t1 (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b0) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb0:B.λw:T.λu:T.eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u))→∀P:Prop.P)
assume t0: T
suppose :
or
ex_3 B T T λb0:B.λw:T.λu:T.eq T t0 (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b0) w u))→∀P:Prop.P
assume t1: T
suppose :
or
ex_3 B T T λb0:B.λw:T.λu:T.eq T t1 (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b0) w u))→∀P:Prop.P
by (refl_equal . .)
we proved eq T (THead (Bind b) t0 t1) (THead (Bind b) t0 t1)
by (ex_3_intro . . . . . . . previous)
we proved ex_3 B T T λb0:B.λw:T.λu:T.eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u)
by (or_introl . . previous)
we proved
or
ex_3 B T T λb0:B.λw:T.λu:T.eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u))→∀P:Prop.P
∀t0:T
.(or
ex_3 B T T λb0:B.λw:T.λu:T.eq T t0 (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b0) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb0:B.λw:T.λu:T.eq T t1 (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b0) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb0:B.λw:T.λu:T.eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u)
∀b0:B.∀w:T.∀u:T.(eq T (THead (Bind b) t0 t1) (THead (Bind b0) w u))→∀P:Prop.P)
case Flat : f:F ⇒
the thesis becomes
∀t0:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t1 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb:B.λw:T.λu:T.eq T (THead (Flat f) t0 t1) (THead (Bind b) w u)
∀b:B
.∀w:T.∀u:T.(eq T (THead (Flat f) t0 t1) (THead (Bind b) w u))→∀P:Prop.P)
assume t0: T
suppose :
or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P
assume t1: T
suppose :
or
ex_3 B T T λb:B.λw:T.λu:T.eq T t1 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b) w u))→∀P:Prop.P
assume b: B
assume w: T
assume u: T
suppose H1: eq T (THead (Flat f) t0 t1) (THead (Bind b) w u)
assume P: Prop
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE THead (Bind b) w u OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat f) t0 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat f) t0 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind b) w u OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
end of H2
consider H2
we proved
<λ:T.Prop>
CASE THead (Bind b) w u OF
TSort ⇒False
| TLRef ⇒False
| THead k0 ⇒<λ:K.Prop> CASE k0 OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved
∀b:B
.∀w:T.∀u:T.(eq T (THead (Flat f) t0 t1) (THead (Bind b) w u))→∀P:Prop.P
by (or_intror . . previous)
we proved
or
ex_3 B T T λb:B.λw:T.λu:T.eq T (THead (Flat f) t0 t1) (THead (Bind b) w u)
∀b:B
.∀w:T.∀u:T.(eq T (THead (Flat f) t0 t1) (THead (Bind b) w u))→∀P:Prop.P
∀t0:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t1 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb:B.λw:T.λu:T.eq T (THead (Flat f) t0 t1) (THead (Bind b) w u)
∀b:B
.∀w:T.∀u:T.(eq T (THead (Flat f) t0 t1) (THead (Bind b) w u))→∀P:Prop.P)
we proved
∀t0:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t1 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb:B.λw:T.λu:T.eq T (THead k t0 t1) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (THead k t0 t1) (THead (Bind b) w u))→∀P:Prop.P)
∀k:K
.∀t0:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t0 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t0 (THead (Bind b) w u))→∀P:Prop.P)
→∀t1:T
.(or
ex_3 B T T λb:B.λw:T.λu:T.eq T t1 (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t1 (THead (Bind b) w u))→∀P:Prop.P)
→(or
ex_3 B T T λb:B.λw:T.λu:T.eq T (THead k t0 t1) (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T (THead k t0 t1) (THead (Bind b) w u))→∀P:Prop.P)
we proved
or
ex_3 B T T λb:B.λw:T.λu:T.eq T t (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t (THead (Bind b) w u))→∀P:Prop.P
we proved
∀t:T
.or
ex_3 B T T λb:B.λw:T.λu:T.eq T t (THead (Bind b) w u)
∀b:B.∀w:T.∀u:T.(eq T t (THead (Bind b) w u))→∀P:Prop.P