X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fnf2%2Fdec.ma;h=eaaf4346a79f3fe3c7bafbf63c777d3b1a10cf09;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=25245ac1170c7ce5b2a56b309f62f12a48fabbfb;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma
index 25245ac11..eaaf4346a 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma
@@ -14,17 +14,15 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/nf2/defs.ma".
 
+include "LambdaDelta-1/pr2/clen.ma".
 
-include "nf2/defs.ma".
+include "LambdaDelta-1/pr2/fwd.ma".
 
-include "pr2/clen.ma".
+include "LambdaDelta-1/pr0/dec.ma".
 
-include "pr2/fwd.ma".
-
-include "pr0/dec.ma".
-
-include "C/props.ma".
+include "LambdaDelta-1/C/props.ma".
 
 theorem nf2_dec:
  \forall (c: C).(\forall (t1: T).(or (nf2 c t1) (ex2 T (\lambda (t2: T).((eq 
@@ -97,7 +95,7 @@ x))).(\lambda (P: Prop).(let H8 \def (eq_ind T t1 (\lambda (t0: T).(subst0
 (clen c0) t t0 (lift (S O) (clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in 
 (subst0_gen_lift_false x t (lift (S O) (clen c0) x) (S O) (clen c0) (clen c0) 
 (le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt 
-(clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen c0) (S O)) (plus_comm 
+(clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen c0) (S O)) (plus_sym 
 (clen c0) (S O))) H8 P)))) (pr2_delta (CTail (Bind Abbr) t c0) (CSort x0) t 
 (clen c0) H6 t1 t1 (pr0_refl t1) (lift (S O) (clen c0) x) H4))))) H5)))) 
 (\lambda (H4: (eq T t1 (lift (S O) (clen c0) x))).(let H5 \def (eq_ind T t1 
@@ -130,7 +128,7 @@ x1)).(let H14 \def (eq_ind T x0 (\lambda (t0: T).(subst0 (clen c0) t t0 t2))
 H11 (lift (S O) (clen c0) x1) H12) in (subst0_gen_lift_false x1 t t2 (S O) 
 (clen c0) (clen c0) (le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) 
 (\lambda (n: nat).(lt (clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen 
-c0) (S O)) (plus_comm (clen c0) (S O))) H14 (eq T (lift (S O) (clen c0) x) 
+c0) (S O)) (plus_sym (clen c0) (S O))) H14 (eq T (lift (S O) (clen c0) x) 
 t2)))))) (pr0_gen_lift x x0 (S O) (clen c0) H10)))))) H8)) H7)))))) t1 H4))) 
 H3))) H2))) (or_introl (\forall (t2: T).((pr2 (CTail (Bind Abst) t c0) t1 t2) 
 \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: