X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2FT%2Fprops.ma;h=9e1bb8cfd01ef6927811a49855c9046358c81286;hb=99f153e43f18bc682339bed41c8230af2ac6fd2f;hp=c9b9619f407fde650546eae49e78aa8e2073747a;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

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 c9b9619f4..9e1bb8cfd 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma
@@ -14,9 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
-
-include "T/defs.ma".
+include "LambdaDelta-1/T/defs.ma".
 
 theorem not_abbr_abst:
  not (eq B Abbr Abst)
@@ -34,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))))