update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / sex_sex.ma

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 19078cfbe6a5ad84435abbd6ff9e3da79768d65b..90ea65aafca4eff6e19ee5a4d1bd5cbd4d949981 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
@@ -52,7 +52,7 @@ theorem sex_trans (RN) (RP) (f):
 /2 width=9 by sex_trans_gen/ qed-.
 
 theorem sex_trans_id_cfull (R1) (R2) (R3):
-        â\88\80L1,L,f. L1 ⪤[R1,cfull,f] L â\86\92 ð\9d\90\88â\9dªfâ\9d« →
+        â\88\80L1,L,f. L1 ⪤[R1,cfull,f] L â\86\92 ð\9d\90\88â\9d¨fâ\9d© →
         ∀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 // ]