Ok, even if not stated formally, now we know that the map from REL to OA is

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma
index 797c1f1db418604a273c2bbbe8cea95962f381a2..50f389929042ebd391ad863dd13f12af960056d3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "subst1/fwd.ma".
+include "LambdaDelta-1/subst1/fwd.ma".
 
-include "subst0/subst0.ma".
+include "LambdaDelta-1/subst0/subst0.ma".
 
 theorem subst1_subst1:
  \forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst1 
@@ -176,7 +176,7 @@ t2))))) (\lambda (H1: (eq T t0 (lift (S O) i t1))).(\lambda (t2: T).(\lambda
 (t: T).(subst1 i u t (lift (S O) i t2))) H2 (lift (S O) i t1) H1) in (let H4 
 \def (sym_eq T (lift (S O) i t2) (lift (S O) i t1) (subst1_gen_lift_eq t1 u 
 (lift (S O) i t2) (S O) i i (le_n i) (eq_ind_r nat (plus (S O) i) (\lambda 
-(n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_comm i (S O))) 
+(n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_sym i (S O))) 
 H3)) in (lift_inj t1 t2 (S O) i H4)))))) (\lambda (t2: T).(\lambda (H1: 
 (subst0 i u t0 t2)).(\lambda (H2: (eq T t2 (lift (S O) i t1))).(\lambda (t3: 
 T).(\lambda (H3: (subst1 i u t0 (lift (S O) i t3))).(let H4 \def (eq_ind T t2 
@@ -188,7 +188,7 @@ t3)) (\lambda (y0: T).(\lambda (H5: (subst1 i u t0 y0)).(subst1_ind i u t0
 T).(subst0 i u t (lift (S O) i t1))) H4 (lift (S O) i t3) H6) in 
 (subst0_gen_lift_false t3 u (lift (S O) i t1) (S O) i i (le_n i) (eq_ind_r 
 nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i 
-(S O)) (plus_comm i (S O))) H7 (eq T t1 t3)))) (\lambda (t4: T).(\lambda (H6: 
+(S O)) (plus_sym i (S O))) H7 (eq T t1 t3)))) (\lambda (t4: T).(\lambda (H6: 
 (subst0 i u t0 t4)).(\lambda (H7: (eq T t4 (lift (S O) i t3))).(let H8 \def 
 (eq_ind T t4 (\lambda (t: T).(subst0 i u t0 t)) H6 (lift (S O) i t3) H7) in 
 (sym_eq T t3 t1 (subst0_confluence_lift t0 t3 u i H8 t1 H4)))))) y0 H5)))