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