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