X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsubst0%2Fdec.ma;h=93aa0736a340c2d11a253bf2d86a051a4c5be284;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=0234ff06c57445ff15f1ee290f1ce4f7ac2d284a;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma b/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma
index 0234ff06c..93aa0736a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst0/dec.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/subst0/defs.ma".
+include "basic_1/subst0/defs.ma".
 
-include "Basic-1/lift/props.ma".
+include "basic_1/lift/props.ma".
 
-theorem dnf_dec2:
+lemma dnf_dec2:
  \forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v: 
 T).(subst0 d w t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S 
 O) d v))))))
@@ -46,8 +46,8 @@ w (TLRef n) (lift (S O) n0 v))))) (ex T (\lambda (v: T).(eq T (TLRef n) (lift
 O) n v)))) (\lambda (w: T).(ex_intro T (\lambda (v: T).(subst0 n w (TLRef n) 
 (lift (S O) n v))) (lift n O w) (eq_ind_r T (lift (plus (S O) n) O w) 
 (\lambda (t0: T).(subst0 n w (TLRef n) t0)) (subst0_lref w n) (lift (S O) n 
-(lift n O w)) (lift_free w n (S O) O n (le_n (plus O n)) (le_O_n n)))))) d 
-H)) (\lambda (H: (lt d n)).(or_intror (\forall (w: T).(ex T (\lambda (v: 
+(lift n O w)) (lift_free w n (S O) O n (le_plus_r O n) (le_O_n n)))))) d H)) 
+(\lambda (H: (lt d n)).(or_intror (\forall (w: T).(ex T (\lambda (v: 
 T).(subst0 d w (TLRef n) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T 
 (TLRef n) (lift (S O) d v)))) (ex_intro T (\lambda (v: T).(eq T (TLRef n) 
 (lift (S O) d v))) (TLRef (pred n)) (eq_ind_r T (TLRef n) (\lambda (t0: 
@@ -147,11 +147,8 @@ 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:
+lemma dnf_dec:
  \forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or 
 (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v)))))))
 \def
@@ -176,7 +173,4 @@ 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 *)