DEFINITION terms_props__bind_dec()
TYPE =
∀b1:B.∀b2:B.(or (eq B b1 b2) (eq B b1 b2)→∀P:Prop.P)
BODY =
assume b1: B
we proceed by induction on b1 to prove ∀b2:B.(or (eq B b1 b2) (eq B b1 b2)→∀P:Prop.P)
case Abbr : ⇒
the thesis becomes ∀b2:B.(or (eq B Abbr b2) (eq B Abbr b2)→∀P:Prop.P)
assume b2: B
we proceed by induction on b2 to prove or (eq B Abbr b2) (eq B Abbr b2)→∀P:Prop.P
case Abbr : ⇒
the thesis becomes or (eq B Abbr Abbr) (eq B Abbr Abbr)→∀P:Prop.P
by (refl_equal . .)
we proved eq B Abbr Abbr
by (or_introl . . previous)
or (eq B Abbr Abbr) (eq B Abbr Abbr)→∀P:Prop.P
case Abst : ⇒
the thesis becomes or (eq B Abbr Abst) (eq B Abbr Abst)→∀P:Prop.P
suppose H: eq B Abbr Abst
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:B.Prop> CASE Abst OF Abbr⇒True | Abst⇒False | Void⇒False
case refl_equal : ⇒
the thesis becomes <λ:B.Prop> CASE Abbr OF Abbr⇒True | Abst⇒False | Void⇒False
consider I
we proved True
<λ:B.Prop> CASE Abbr OF Abbr⇒True | Abst⇒False | Void⇒False
<λ:B.Prop> CASE Abst OF Abbr⇒True | Abst⇒False | Void⇒False
end of H0
consider H0
we proved <λ:B.Prop> CASE Abst OF Abbr⇒True | Abst⇒False | Void⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq B Abbr Abst)→∀P:Prop.P
by (or_intror . . previous)
or (eq B Abbr Abst) (eq B Abbr Abst)→∀P:Prop.P
case Void : ⇒
the thesis becomes or (eq B Abbr Void) (eq B Abbr Void)→∀P:Prop.P
suppose H: eq B Abbr Void
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:B.Prop> CASE Void OF Abbr⇒True | Abst⇒False | Void⇒False
case refl_equal : ⇒
the thesis becomes <λ:B.Prop> CASE Abbr OF Abbr⇒True | Abst⇒False | Void⇒False
consider I
we proved True
<λ:B.Prop> CASE Abbr OF Abbr⇒True | Abst⇒False | Void⇒False
<λ:B.Prop> CASE Void OF Abbr⇒True | Abst⇒False | Void⇒False
end of H0
consider H0
we proved <λ:B.Prop> CASE Void OF Abbr⇒True | Abst⇒False | Void⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq B Abbr Void)→∀P:Prop.P
by (or_intror . . previous)
or (eq B Abbr Void) (eq B Abbr Void)→∀P:Prop.P
we proved or (eq B Abbr b2) (eq B Abbr b2)→∀P:Prop.P
∀b2:B.(or (eq B Abbr b2) (eq B Abbr b2)→∀P:Prop.P)
case Abst : ⇒
the thesis becomes ∀b2:B.(or (eq B Abst b2) (eq B Abst b2)→∀P:Prop.P)
assume b2: B
we proceed by induction on b2 to prove or (eq B Abst b2) (eq B Abst b2)→∀P:Prop.P
case Abbr : ⇒
the thesis becomes or (eq B Abst Abbr) (eq B Abst Abbr)→∀P:Prop.P
suppose H: eq B Abst Abbr
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:B.Prop> CASE Abbr OF Abbr⇒False | Abst⇒True | Void⇒False
case refl_equal : ⇒
the thesis becomes <λ:B.Prop> CASE Abst OF Abbr⇒False | Abst⇒True | Void⇒False
consider I
we proved True
<λ:B.Prop> CASE Abst OF Abbr⇒False | Abst⇒True | Void⇒False
<λ:B.Prop> CASE Abbr OF Abbr⇒False | Abst⇒True | Void⇒False
end of H0
consider H0
we proved <λ:B.Prop> CASE Abbr OF Abbr⇒False | Abst⇒True | Void⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq B Abst Abbr)→∀P:Prop.P
by (or_intror . . previous)
or (eq B Abst Abbr) (eq B Abst Abbr)→∀P:Prop.P
case Abst : ⇒
the thesis becomes or (eq B Abst Abst) (eq B Abst Abst)→∀P:Prop.P
by (refl_equal . .)
we proved eq B Abst Abst
by (or_introl . . previous)
or (eq B Abst Abst) (eq B Abst Abst)→∀P:Prop.P
case Void : ⇒
the thesis becomes or (eq B Abst Void) (eq B Abst Void)→∀P:Prop.P
suppose H: eq B Abst Void
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:B.Prop> CASE Void OF Abbr⇒False | Abst⇒True | Void⇒False
case refl_equal : ⇒
the thesis becomes <λ:B.Prop> CASE Abst OF Abbr⇒False | Abst⇒True | Void⇒False
consider I
we proved True
<λ:B.Prop> CASE Abst OF Abbr⇒False | Abst⇒True | Void⇒False
<λ:B.Prop> CASE Void OF Abbr⇒False | Abst⇒True | Void⇒False
end of H0
consider H0
we proved <λ:B.Prop> CASE Void OF Abbr⇒False | Abst⇒True | Void⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq B Abst Void)→∀P:Prop.P
by (or_intror . . previous)
or (eq B Abst Void) (eq B Abst Void)→∀P:Prop.P
we proved or (eq B Abst b2) (eq B Abst b2)→∀P:Prop.P
∀b2:B.(or (eq B Abst b2) (eq B Abst b2)→∀P:Prop.P)
case Void : ⇒
the thesis becomes ∀b2:B.(or (eq B Void b2) (eq B Void b2)→∀P:Prop.P)
assume b2: B
we proceed by induction on b2 to prove or (eq B Void b2) (eq B Void b2)→∀P:Prop.P
case Abbr : ⇒
the thesis becomes or (eq B Void Abbr) (eq B Void Abbr)→∀P:Prop.P
suppose H: eq B Void Abbr
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:B.Prop> CASE Abbr OF Abbr⇒False | Abst⇒False | Void⇒True
case refl_equal : ⇒
the thesis becomes <λ:B.Prop> CASE Void OF Abbr⇒False | Abst⇒False | Void⇒True
consider I
we proved True
<λ:B.Prop> CASE Void OF Abbr⇒False | Abst⇒False | Void⇒True
<λ:B.Prop> CASE Abbr OF Abbr⇒False | Abst⇒False | Void⇒True
end of H0
consider H0
we proved <λ:B.Prop> CASE Abbr OF Abbr⇒False | Abst⇒False | Void⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq B Void Abbr)→∀P:Prop.P
by (or_intror . . previous)
or (eq B Void Abbr) (eq B Void Abbr)→∀P:Prop.P
case Abst : ⇒
the thesis becomes or (eq B Void Abst) (eq B Void Abst)→∀P:Prop.P
suppose H: eq B Void Abst
assume P: Prop
(H0)
we proceed by induction on H to prove <λ:B.Prop> CASE Abst OF Abbr⇒False | Abst⇒False | Void⇒True
case refl_equal : ⇒
the thesis becomes <λ:B.Prop> CASE Void OF Abbr⇒False | Abst⇒False | Void⇒True
consider I
we proved True
<λ:B.Prop> CASE Void OF Abbr⇒False | Abst⇒False | Void⇒True
<λ:B.Prop> CASE Abst OF Abbr⇒False | Abst⇒False | Void⇒True
end of H0
consider H0
we proved <λ:B.Prop> CASE Abst OF Abbr⇒False | Abst⇒False | Void⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq B Void Abst)→∀P:Prop.P
by (or_intror . . previous)
or (eq B Void Abst) (eq B Void Abst)→∀P:Prop.P
case Void : ⇒
the thesis becomes or (eq B Void Void) (eq B Void Void)→∀P:Prop.P
by (refl_equal . .)
we proved eq B Void Void
by (or_introl . . previous)
or (eq B Void Void) (eq B Void Void)→∀P:Prop.P
we proved or (eq B Void b2) (eq B Void b2)→∀P:Prop.P
∀b2:B.(or (eq B Void b2) (eq B Void b2)→∀P:Prop.P)
we proved ∀b2:B.(or (eq B b1 b2) (eq B b1 b2)→∀P:Prop.P)
we proved ∀b1:B.∀b2:B.(or (eq B b1 b2) (eq B b1 b2)→∀P:Prop.P)