- some bugs fixed in the domain-based preorders on environments

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / T / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma
index 575d918aa0e433905ccae7afd39efa9de9bb668d..9e1bb8cfd01ef6927811a49855c9046358c81286 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma
@@ -32,6 +32,22 @@ B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
 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))))