Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma
index 36c004667b38283c503970d7d3eb1e4ba8c0b64e..236215b2265eb2ba5e14caf97074fb0990593e0c 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma
@@ -71,10 +71,10 @@ O w)))) (eq_ind_r T (lift (plus h (S i)) O w) (\lambda (t: T).(tau0 g c0
 (TLRef (plus i h)) t)) (eq_ind_r nat (plus (S i) h) (\lambda (n: nat).(tau0 g 
 c0 (TLRef (plus i h)) (lift n O w))) (tau0_abbr g c0 d v (plus i h) 
 (drop_getl_trans_ge i c0 c d0 h H3 (CHead d (Bind Abbr) v) H0 H4) w H1) (plus 
-h (S i)) (plus_comm h (S i))) (lift h d0 (lift (S i) O w)) (lift_free w (S i) 
+h (S i)) (plus_sym h (S i))) (lift h d0 (lift (S i) O w)) (lift_free w (S i) 
 h O d0 (le_S d0 i H4) (le_O_n d0))) (plus i (S O)) (eq_ind_r nat (plus (S O) 
 i) (\lambda (n: nat).(eq nat (S i) n)) (refl_equal nat (plus (S O) i)) (plus 
-i (S O)) (plus_comm i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h d0 
+i (S O)) (plus_sym i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h d0 
 H4)))))))))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda 
 (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abst) v))).(\lambda (w: 
 T).(\lambda (H1: (tau0 g d v w)).(\lambda (H2: ((\forall (c0: C).(\forall (h: 
@@ -114,10 +114,10 @@ O v)))) (eq_ind_r T (lift (plus h (S i)) O v) (\lambda (t: T).(tau0 g c0
 (TLRef (plus i h)) t)) (eq_ind_r nat (plus (S i) h) (\lambda (n: nat).(tau0 g 
 c0 (TLRef (plus i h)) (lift n O v))) (tau0_abst g c0 d v (plus i h) 
 (drop_getl_trans_ge i c0 c d0 h H3 (CHead d (Bind Abst) v) H0 H4) w H1) (plus 
-h (S i)) (plus_comm h (S i))) (lift h d0 (lift (S i) O v)) (lift_free v (S i) 
+h (S i)) (plus_sym h (S i))) (lift h d0 (lift (S i) O v)) (lift_free v (S i) 
 h O d0 (le_S d0 i H4) (le_O_n d0))) (plus i (S O)) (eq_ind_r nat (plus (S O) 
 i) (\lambda (n: nat).(eq nat (S i) n)) (refl_equal nat (plus (S O) i)) (plus 
-i (S O)) (plus_comm i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h d0 
+i (S O)) (plus_sym i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h d0 
 H4)))))))))))))))) (\lambda (b: B).(\lambda (c: C).(\lambda (v: T).(\lambda 
 (t3: T).(\lambda (t4: T).(\lambda (_: (tau0 g (CHead c (Bind b) v) t3 
 t4)).(\lambda (H1: ((\forall (c0: C).(\forall (h: nat).(\forall (d: