X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Flift1%2Fprops.ma;h=8f399a0fd18042df184855254df61a5db610e551;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=216c6d80b8c869d82424f67ac682a0930b8a6f3a;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
index 216c6d80b..8f399a0fd 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
@@ -14,13 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/props".
+include "LambdaDelta-1/lift/props.ma".
 
-include "lift1/defs.ma".
-
-include "lift/props.ma".
-
-include "drop1/defs.ma".
+include "LambdaDelta-1/drop1/defs.ma".
 
 theorem lift1_lift1:
  \forall (is1: PList).(\forall (is2: PList).(\forall (t: T).(eq T (lift1 is1 
@@ -31,13 +27,9 @@ PList).(\forall (t: T).(eq T (lift1 p (lift1 is2 t)) (lift1 (papp p is2)
 t))))) (\lambda (is2: PList).(\lambda (t: T).(refl_equal T (lift1 is2 t)))) 
 (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: 
 ((\forall (is2: PList).(\forall (t: T).(eq T (lift1 p (lift1 is2 t)) (lift1 
-(papp p is2) t)))))).(\lambda (is2: PList).(\lambda (t: T).(sym_eq T (lift n 
-n0 (lift1 (papp p is2) t)) (lift n n0 (lift1 p (lift1 is2 t))) (sym_eq T 
-(lift n n0 (lift1 p (lift1 is2 t))) (lift n n0 (lift1 (papp p is2) t)) 
-(sym_eq T (lift n n0 (lift1 (papp p is2) t)) (lift n n0 (lift1 p (lift1 is2 
-t))) (f_equal3 nat nat T T lift n n n0 n0 (lift1 (papp p is2) t) (lift1 p 
-(lift1 is2 t)) (refl_equal nat n) (refl_equal nat n0) (sym_eq T (lift1 p 
-(lift1 is2 t)) (lift1 (papp p is2) t) (H is2 t)))))))))))) is1).
+(papp p is2) t)))))).(\lambda (is2: PList).(\lambda (t: T).(f_equal3 nat nat 
+T T lift n n n0 n0 (lift1 p (lift1 is2 t)) (lift1 (papp p is2) t) (refl_equal 
+nat n) (refl_equal nat n0) (H is2 t)))))))) is1).
 
 theorem lift1_xhg:
  \forall (hds: PList).(\forall (t: T).(eq T (lift1 (Ss hds) (lift (S O) O t)) 
@@ -122,14 +114,14 @@ t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t))))
 (eq_ind_r nat (plus (trans hds0 i) h) (\lambda (n: nat).(eq T (lift (S n) O 
 (lift1 (ptrans hds0 i) t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans 
 hds0 i) t)))) (refl_equal T (lift (S (plus (trans hds0 i) h)) O (lift1 
-(ptrans hds0 i) t))) (plus h (trans hds0 i)) (plus_comm h (trans hds0 i))) 
+(ptrans hds0 i) t))) (plus h (trans hds0 i)) (plus_sym h (trans hds0 i))) 
 (plus h (S (trans hds0 i))) (plus_n_Sm h (trans hds0 i))) (lift h d (lift (S 
 (trans hds0 i)) O (lift1 (ptrans hds0 i) t))) (lift_free (lift1 (ptrans hds0 
 i) t) (S (trans hds0 i)) h O d (eq_ind nat (S (plus O (trans hds0 i))) 
 (\lambda (n: nat).(le d n)) (eq_ind_r nat (plus (trans hds0 i) O) (\lambda 
 (n: nat).(le d (S n))) (le_S d (plus (trans hds0 i) O) (le_plus_trans d 
 (trans hds0 i) O (bge_le d (trans hds0 i) H0))) (plus O (trans hds0 i)) 
-(plus_comm O (trans hds0 i))) (plus O (S (trans hds0 i))) (plus_n_Sm O (trans 
+(plus_sym O (trans hds0 i))) (plus O (S (trans hds0 i))) (plus_n_Sm O (trans 
 hds0 i))) (le_O_n d)))) x_x))) (lift1 hds0 (lift (S i) O t)) (H i t)))))))) 
 hds).