eq over SET1 and SET no longer used

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / subst1 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma
index f16462a86aa20a7e52677886bca45c6d1326a04f..cb13ac64451b5dff408db314070afd7bd6802767 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "subst1/defs.ma".
+include "LambdaDelta-1/subst1/defs.ma".
 
-include "subst0/props.ma".
+include "LambdaDelta-1/subst0/props.ma".
 
 theorem subst1_head:
  \forall (v: T).(\forall (u1: T).(\forall (u2: T).(\forall (i: nat).((subst1 
@@ -138,7 +138,7 @@ nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O
 (TLRef h) (TLRef n) (lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n)) 
 (TLRef (plus h (S n))) (lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n)) 
 (sym_eq nat (S (plus h n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h) 
-(plus_comm n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) 
+(plus_sym n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) 
 (lift_lref_ge n (S h) n (le_n n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt 
 n (S h) (S n) (le_n (S n)))) i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T 
 (TLRef (plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i