X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fsex_sex.ma;h=e75771c2350c7990e9d10cdfcd819dda35adc730;hp=239966181fd18c1e0adf4cc34c0f5b9e2de3b741;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
index 239966181..e75771c23 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
@@ -21,8 +21,8 @@ include "static_2/relocation/drops.ma".
 
 theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP):
                       ∀L1,f.
-                      (∀g,I,K,n. ⇩*[n] L1 ≘ K.ⓘ{I} → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
-                      (∀g,I,K,n. ⇩*[n] L1 ≘ K.ⓘ{I} → ⫯g = ⫱*[n] f → sex_transitive RP1 RP2 RP RN1 RP1 g K I) →
+                      (∀g,I,K,n. ⇩*[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
+                      (∀g,I,K,n. ⇩*[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → sex_transitive RP1 RP2 RP RN1 RP1 g K I) →
                       ∀L0. L1 ⪤[RN1,RP1,f] L0 →
                       ∀L2. L0 ⪤[RN2,RP2,f] L2 →
                       L1 ⪤[RN,RP,f] L2.
@@ -50,7 +50,7 @@ theorem sex_trans (RN) (RP) (f): (∀g,I,K. sex_transitive RN RN RN RN RP g K I)
                                  Transitive … (sex RN RP f).
 /2 width=9 by sex_trans_gen/ qed-.
 
-theorem sex_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈⦃f⦄ →
+theorem sex_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈❪f❫ →
                             ∀L2. L ⪤[R2,cfull,f] L2 → L1 ⪤[R3,cfull,f] L2.
 #R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
 [ #f #Hf #L2 #H >(sex_inv_atom1 … H) -L2 // ]
@@ -62,8 +62,8 @@ qed-.
 
 theorem sex_conf (RN1) (RP1) (RN2) (RP2):
                  ∀L,f.
-                 (∀g,I,K,n. ⇩*[n] L ≘ K.ⓘ{I} → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
-                 (∀g,I,K,n. ⇩*[n] L ≘ K.ⓘ{I} → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
+                 (∀g,I,K,n. ⇩*[n] L ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
+                 (∀g,I,K,n. ⇩*[n] L ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
                  pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L.
 #RN1 #RP1 #RN2 #RP2 #L elim L -L
 [ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1