]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma
update in ground, static_2 and apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_after_isi.ma
index 494659038632fdde6014c105ce8c478ff8736818..f5457f3c335aa58659f6427672392916102b986d 100644 (file)
@@ -41,12 +41,12 @@ qed.
 
 (*** after_isid_inv_sn *)
 lemma pr_after_isi_inv_sn:
-      â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89¡ f.
+      â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89\90 f.
 /3 width=6 by pr_after_isi_sn, pr_after_mono/ qed-.
 
 (*** after_isid_inv_dx *)
 lemma pr_after_isi_inv_dx:
-      â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89¡ f.
+      â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89\90 f.
 /3 width=6 by pr_after_isi_dx, pr_after_mono/ qed-.
 
 (*** after_fwd_isid1 *)