update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream_coafter.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
index 4c141a301d120a3f738699bde659176677aaad91..c158f25930fe6d454e3b0f6884e7d3b3358b0126 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
@@ -89,7 +89,7 @@ qed-.
 
 (* Specific properties on coafter *******************************************)
 
-corec lemma coafter_total_aux: â\88\80f2,f1,f. f2 ~â\88\98 f1 = f â\86\92 f2 ~â\8a\9a f1 â\89¡ f.
+corec lemma coafter_total_aux: â\88\80f2,f1,f. f2 ~â\88\98 f1 = f â\86\92 f2 ~â\8a\9a f1 â\89\98 f.
 * #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
 [ cases n1 -n1
   [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
@@ -99,5 +99,5 @@ corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≡ f.
 ]
 qed-.
 
-theorem coafter_total: â\88\80f2,f1. f2 ~â\8a\9a f1 â\89¡ f2 ~∘ f1.
+theorem coafter_total: â\88\80f2,f1. f2 ~â\8a\9a f1 â\89\98 f2 ~∘ f1.
 /2 width=1 by coafter_total_aux/ qed.