X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2FT%2Fprops.ma;h=9e1bb8cfd01ef6927811a49855c9046358c81286;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=1c661524e92f51ade8d99f53179f7d80f16f9d47;hpb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;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 1c661524e..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 *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/props".
-
-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))))