update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_after_ist_isi.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
index ea312f5a018fb569a5e3b59b8892f94a6ee566e0..4e17044dea05cf49e17b1572967a9294555eadc4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_after_ist.ma".
 
 (*** after_fwd_isid_sn *)
 lemma pr_after_des_ist_eq_sn:
-      â\88\80f2,f1,f. ð\9d\90\93â\9dªfâ\9d« â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f1 â\89¡ f â\86\92 ð\9d\90\88â\9dªf2â\9d«.
+      â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f1 â\89¡ f â\86\92 ð\9d\90\88â\9d¨f2â\9d©.
 #f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H @pr_isi_pat_total // -Hf2
 #i2 #i #Hf2 elim (Hf1 i2) -Hf1
@@ -32,7 +32,7 @@ qed-.
 
 (*** after_fwd_isid_dx *)
 lemma pr_after_des_ist_eq_dx:
-      â\88\80f2,f1,f.  ð\9d\90\93â\9dªfâ\9d« â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\89¡ f â\86\92 ð\9d\90\88â\9dªf1â\9d«.
+      â\88\80f2,f1,f.  ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\89¡ f â\86\92 ð\9d\90\88â\9d¨f1â\9d©.
 #f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H2 @pr_isi_pat_total // -Hf1
 #i1 #i2 #Hi12 elim (pr_after_des_ist_pat … Hi12 … Hf) -f1