update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
index 13681ff13aa44205750b319145b2a8dd3002231e..d627e2597ba3c705f1f68a5f3d3884da9b113f00 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
@@ -20,14 +20,14 @@ include "ground/relocation/pr_coafter_nat_tls.ma".
 
 (*** H_coafter_inj *)
 definition H_pr_coafter_inj: predicate pr_map ≝
-           λf1. ð\9d\90\93â\9dªf1â\9d« →
+           λf1. ð\9d\90\93â\9d¨f1â\9d© →
            ∀f,f21,f22. f1 ~⊚ f21 ≘ f → f1 ~⊚ f22 ≘ f → f21 ≡ f22.
 
 (* Main destructions with pr_ist ********************************************)
 
 (*** coafter_inj_O_aux *)
 corec fact pr_coafter_inj_unit_aux:
-           â\88\80f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ 𝟏 → H_pr_coafter_inj f1.
+           â\88\80f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ 𝟏 → H_pr_coafter_inj f1.
 #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
 cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
 lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
@@ -44,8 +44,8 @@ qed-.
 
 (*** coafter_inj_aux *)
 fact pr_coafter_inj_aux:
-     (â\88\80f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ 𝟏 → H_pr_coafter_inj f1) →
-     â\88\80i2,f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ i2 → H_pr_coafter_inj f1.
+     (â\88\80f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ 𝟏 → H_pr_coafter_inj f1) →
+     â\88\80i2,f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ i2 → H_pr_coafter_inj f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1