]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
update in ground, static_2 and apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_pat_id.ma
index a63fb9355c78d75074077a4b0c0e358253693026..0134687965d50e37f50bcbf42e34bab3224eb1c3 100644 (file)
@@ -27,6 +27,6 @@ lemma pr_pat_id (i): @❨i,𝐢❩ ≘ i.
 
 (*** id_inv_at *)
 lemma pr_pat_inv_id (f):
-      (â\88\80i. @â\9d¨i,fâ\9d© â\89\98 i) â\86\92 ð\9d\90¢ â\89¡ f.
+      (â\88\80i. @â\9d¨i,fâ\9d© â\89\98 i) â\86\92 ð\9d\90¢ â\89\90 f.
 /3 width=1 by pr_pat_inv_eq, pr_id_eq/
 qed-.