update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
index de3ecfe4ee36593fe71d4fff1f8c7e281968c724..a65f972bb89d9bb5dbd561c8094d3e30e88fdd13 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -23,7 +23,7 @@ include "ground/relocation/pr_ist.ma".
 (* Advanced constructions with pr_pat ***************************************)
 
 (*** at_dec *)
-lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (@❨i1,f❩ ≘ i2).
+lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (＠⧣❨i1,f❩ ≘ i2).
 #f #i1 #i2 #Hf lapply (Hf i1) -Hf *
 #j2 #Hf elim (eq_pnat_dec i2 j2)
 [ #H destruct /2 width=1 by or_introl/
@@ -32,9 +32,9 @@ lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (@❨i1,f❩ ≘ i2).
 qed-.
 
 (*** is_at_dec *)
-lemma is_pr_pat_dec (f) (i2): 𝐓❨f❩ → Decidable (∃i1. @❨i1,f❩ ≘ i2).
+lemma is_pr_pat_dec (f) (i2): 𝐓❨f❩ → Decidable (∃i1. ＠⧣❨i1,f❩ ≘ i2).
 #f #i2 #Hf
-lapply (dec_plt (λi1.@❨i1,f❩ ≘ i2) … (↑i2)) [| * ]
+lapply (dec_plt (λi1.＠⧣❨i1,f❩ ≘ i2) … (↑i2)) [| * ]
 [ /2 width=1 by pr_pat_dec/
 | * /3 width=2 by ex_intro, or_introl/
 | #H @or_intror * #i1 #Hi12
@@ -46,7 +46,7 @@ qed-.
 
 (*** at_ext *)
 corec theorem pr_eq_ext_pat (f1) (f2): 𝐓❨f1❩ → 𝐓❨f2❩ →
-              (∀i,i1,i2. @❨i,f1❩ ≘ i1 → @❨i,f2❩ ≘ i2 → i1 = i2) →
+              (∀i,i1,i2. ＠⧣❨i,f1❩ ≘ i1 → ＠⧣❨i,f2❩ ≘ i2 → i1 = i2) →
               f1 ≐ f2.
 cases (pr_map_split_tl f1) #H1
 cases (pr_map_split_tl f2) #H2