X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsubst0%2Fdec.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsubst0%2Fdec.ma;h=0234ff06c57445ff15f1ee290f1ce4f7ac2d284a;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=d93394c4af5612b31bbb31fdabf6b4c965c2c97c;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/dec.ma
index d93394c4a..0234ff06c 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/dec.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/subst0/defs.ma".
+include "Basic-1/subst0/defs.ma".
 
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
 
 theorem dnf_dec2:
  \forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v: 
@@ -147,6 +147,9 @@ x) (lift (S O) (s k d) x0)) (\lambda (t2: T).(eq T (THead k (lift (S O) d x)
 (lift (S O) (s k d) x0)) t2)) (refl_equal T (THead k (lift (S O) d x) (lift 
 (S O) (s k d) x0))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O) 
 d)))) t0 H3) t1 H6))) H5)) H4))))) H2)) H1))))))))) t).
+(* COMMENTS
+Initial nodes: 3549
+END *)
 
 theorem dnf_dec:
  \forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or 
@@ -173,4 +176,7 @@ T).(or (subst0 d w (lift (S O) d x) (lift (S O) d v)) (eq T (lift (S O) d x)
 (lift (S O) d v)))) x (or_intror (subst0 d w (lift (S O) d x) (lift (S O) d 
 x)) (eq T (lift (S O) d x) (lift (S O) d x)) (refl_equal T (lift (S O) d 
 x)))) t H1))) H0)) H))))).
+(* COMMENTS
+Initial nodes: 603
+END *)