update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
index 34fec06e4d9ad8fa5455fd39fbfcdfc87ebd4f40..c58c16172803d1778b22ce7b889956149d39d3e4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_pat.ma".
 
 (*** at_increasing *)
 lemma pr_pat_increasing (i2) (i1) (f):
-      @â\9dªi1,fâ\9d« ≘ i2 → i1 ≤ i2.
+      @â\9d¨i1,fâ\9d© ≘ i2 → i1 ≤ i2.
 #i2 elim i2 -i2
 [ #i1 #f #Hf elim (pr_pat_inv_unit_dx … Hf) -Hf //
 | #i2 #IH * //
@@ -33,14 +33,14 @@ qed-.
 
 (*** at_increasing_strict *)
 lemma pr_pat_increasing_strict (g) (i1) (i2):
-      @â\9dªi1,gâ\9d« ≘ i2 → ∀f. ↑f = g →
-      â\88§â\88§ i1 < i2 & @â\9dªi1,fâ\9d« ≘ ↓i2.
+      @â\9d¨i1,gâ\9d© ≘ i2 → ∀f. ↑f = g →
+      â\88§â\88§ i1 < i2 & @â\9d¨i1,fâ\9d© ≘ ↓i2.
 #g #i1 #i2 #Hg #f #H elim (pr_pat_inv_next … Hg … H) -Hg -H
 /4 width=2 by conj, pr_pat_increasing, ple_succ_bi/
 qed-.
 
 (*** at_fwd_id_ex *)
-lemma pr_pat_des_id (f) (i): @â\9dªi,fâ\9d« ≘ i → ⫯⫰f = f.
+lemma pr_pat_des_id (f) (i): @â\9d¨i,fâ\9d© ≘ i → ⫯⫰f = f.
 #f elim (pr_map_split_tl f) //
 #H #i #Hf elim (pr_pat_inv_next … Hf … H) -Hf -H
 #j2 #Hg #H destruct lapply (pr_pat_increasing … Hg) -Hg
@@ -51,8 +51,8 @@ qed-.
 
 (*** at_le_ex *)
 lemma pr_pat_le_ex (j2) (i2) (f):
-      @â\9dªi2,fâ\9d« ≘ j2 → ∀i1. i1 ≤ i2 →
-      â\88\83â\88\83j1. @â\9dªi1,fâ\9d« ≘ j1 & j1 ≤ j2.
+      @â\9d¨i2,fâ\9d© ≘ j2 → ∀i1. i1 ≤ i2 →
+      â\88\83â\88\83j1. @â\9d¨i1,fâ\9d© ≘ j1 & j1 ≤ j2.
 #j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
 [ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3: * |*: // ]
   #g [ #x2 ] #Hg [ #H2 ] #H0
@@ -71,7 +71,7 @@ qed-.
 
 (*** at_id_le *)
 lemma pr_pat_id_le (i1) (i2):
-      i1 â\89¤ i2 â\86\92 â\88\80f. @â\9dªi2,fâ\9d« â\89\98 i2 â\86\92 @â\9dªi1,fâ\9d« ≘ i1.
+      i1 â\89¤ i2 â\86\92 â\88\80f. @â\9d¨i2,fâ\9d© â\89\98 i2 â\86\92 @â\9d¨i1,fâ\9d© ≘ i1.
 #i1 #i2 #H
 @(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ] #f #Hf
 lapply (pr_pat_des_id … Hf) #H <H in Hf; -H