DEFINITION not_abst_void()
TYPE =
       not (eq B Abst Void)
BODY =
       we must prove not (eq B Abst Void)
       or equivalently (eq B Abst Void)→False
       suppose H: eq B Abst Void
          (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 False
          we proved False
       we proved (eq B Abst Void)→False
       that is equivalent to not (eq B Abst Void)