update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_coafter_ist_isi.ma
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma

index d3dc9e6e1365d0df21fa034c83702dbd11567b14..50a68b5fbfa1bc65b58438bf42619ba283b4c0a5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
@@ -21,13 +21,13 @@ include "ground/relocation/pr_coafter_nat_tls.ma".
  
  (*** H_coafter_fwd_isid2 *)
  definition H_pr_coafter_des_ist_sn_isi: predicate pr_map ≝
-           Î»f1. â\88\80f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\93â\9dªf1â\9d« â\86\92 ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªf2â\9d«.
+           Î»f1. â\88\80f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\93â\9d¨f1â\9d© â\86\92 ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90\88â\9d¨f2â\9d©.
  
  (* Destructions with pr_ist and pr_isi **************************************)
  
  (*** coafter_fwd_isid2_O_aux *)
  corec fact pr_coafter_des_ist_sn_isi_unit_aux:
-           â\88\80f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
+           â\88\80f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
  #f1 #H1f1 #f2 #f #H #H2f1 #Hf
  cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
  lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
@@ -42,8 +42,8 @@ qed-.
  
  (*** coafter_fwd_isid2_aux *)
  fact pr_coafter_des_ist_sn_isi_aux:
-     (â\88\80f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
-     â\88\80i2,f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
+     (â\88\80f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
+     â\88\80i2,f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
  #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
  #i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
  elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1