Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind
False H0)).
+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)).
+
theorem thead_x_y_y:
\forall (k: K).(\forall (v: T).(\forall (t: T).((eq T (THead k v t) t) \to
(\forall (P: Prop).P))))