]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
update in ground, static_2 and apps_2
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_isu_uni.ma
index 1e6706a8bb8207db4234aaadab22f7a110c384e6..bb4cceedea88d5cc9dcc40a319573e43e5964484 100644 (file)
@@ -43,7 +43,7 @@ lemma pr_isu_eq_repl_fwd:
 (* Inversions with pr_uni ***************************************************)
 
 (*** uni_isuni *)
-lemma pr_isu_inv_uni (f): ð\9d\90\94â\9d¨fâ\9d© â\86\92 â\88\83n. ð\9d\90®â\9d¨nâ\9d© â\89¡ f.
+lemma pr_isu_inv_uni (f): ð\9d\90\94â\9d¨fâ\9d© â\86\92 â\88\83n. ð\9d\90®â\9d¨nâ\9d© â\89\90 f.
 #f #H elim H -f
 [ /3 width=2 by pr_isi_inv_uni, ex_intro/
 | #f #_ #g #H * /3 width=6 by pr_eq_next, ex_intro/