]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_after_uni.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_after_uni.ma
index e74d8e0f7eedbb53822842042f4ffc47efdca2c6..6d962f5c89e04d300eebf1506eca6eed3ca6a56d 100644 (file)
@@ -35,7 +35,7 @@ lemma pr_after_uni_sn_pushs (h):
 qed.
 
 lemma pr_after_uni_isi_next (h1):
-      â\88\80f2. ð\9d\90\88â\9dªf2â\9d« → 𝐮❨h1❩ ⊚ ↑f2 ≘ ↑𝐮❨h1❩.
+      â\88\80f2. ð\9d\90\88â\9d¨f2â\9d© → 𝐮❨h1❩ ⊚ ↑f2 ≘ ↑𝐮❨h1❩.
 #h1 @(nat_ind_succ … h1) -h1
 /5 width=7 by pr_after_isi_dx, pr_after_eq_repl_back_sn, pr_after_next, pr_after_push, pr_isi_inv_eq_push/
 qed.