update in ground, static_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
index 869486b4afe700596ed9ecbea6f3caa63a44f940..262fe616731ffa3f1677273c0f6a6236692d6ea7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma
@@ -19,7 +19,7 @@ include "ground/relocation/tr_nexts.ma".
 
 (* Constructions with pr_eq and stream_eq ***********************************)
 
-corec lemma eq_tr_inj_bi (f1) (f2): f1 â\89\97 f2 â\86\92 ð\9d\90­â\9d¨f1â\9d© â\89¡ 𝐭❨f2❩.
+corec lemma eq_tr_inj_bi (f1) (f2): f1 â\89\97 f2 â\86\92 ð\9d\90­â\9d¨f1â\9d© â\89\90 𝐭❨f2❩.
 * -f1 -f2 #p1 #p2 #f1 #f2 * -p2 #H
 cases p1 -p1
 [ @pr_eq_push /2 width=5 by/
@@ -31,7 +31,7 @@ qed.
 
 (* Inversions with pr_eq and stream_eq **************************************)
 
-corec lemma eq_inv_tr_inj_bi (f1) (f2): ð\9d\90­â\9d¨f1â\9d© â\89¡ 𝐭❨f2❩ → f1 ≗ f2.
+corec lemma eq_inv_tr_inj_bi (f1) (f2): ð\9d\90­â\9d¨f1â\9d© â\89\90 𝐭❨f2❩ → f1 ≗ f2.
 cases f1 -f1 #p1 #f1 cases f2 -f2 #p2 #f2
 cases tr_inj_unfold cases tr_inj_unfold #H
 cases (pr_eq_inv_nexts_push_bi … H) -H #H1 #H2