+theorem not_abbr_void:
+ not (eq B Abbr Void)
+\def
+ \lambda (H: (eq B Abbr Void)).(let H0 \def (eq_ind B Abbr (\lambda (ee:
+B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow True |
+Abst \Rightarrow False | Void \Rightarrow False])) I Void H) in (False_ind
+False H0)).
+
+theorem not_abst_void:
+ not (eq B Abst Void)
+\def
+ \lambda (H: (eq B Abst Void)).(let H0 \def (eq_ind B Abst (\lambda (ee:
+B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
+Abst \Rightarrow True | Void \Rightarrow False])) I Void H) in (False_ind
+False H0)).
+