]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / sex.ma
index 47912ace088d171406a07842e3ed6c36bcb6cb69..c51389ea8ff42e82d1f7162e659cb9770f41bac0 100644 (file)
@@ -242,7 +242,7 @@ qed-.
 
 lemma sex_co_isid (RN1) (RP1) (RN2) (RP2):
       RP1 ⊆ RP2 →
-      â\88\80f,L1,L2. L1 âª¤[RN1,RP1,f] L2 â\86\92 ð\9d\90\88â\9dªfâ\9d« →
+      â\88\80f,L1,L2. L1 âª¤[RN1,RP1,f] L2 â\86\92 ð\9d\90\88â\9d¨fâ\9d© →
       L1 ⪤[RN2,RP2,f] L2.
 #RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
 #f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H