]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
made executable again
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_sle_eq.ma
index 383ad127fae9e2bf0025d060d10e79a3b4812f41..aa826268ead1e14fe49a7bfbc7d2341541c264cb 100644 (file)
@@ -56,5 +56,5 @@ qed-.
 
 (*** sle_refl_eq *)
 lemma pr_sle_refl_eq:
-      â\88\80f1,f2. f1 â\89¡ f2 → f1 ⊆ f2.
+      â\88\80f1,f2. f1 â\89\90 f2 → f1 ⊆ f2.
 /2 width=3 by pr_sle_eq_repl_back_dx/ qed.