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 a65f972bb89d9bb5dbd561c8094d3e30e88fdd13..dd2380cb726b1fbd8b532aa0e2e30c55a033769e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -70,7 +70,7 @@ qed-.
 
 (* Advanced constructions with pr_nat ***************************************)
 
-lemma is_pr_nat_dec (f) (l2): 𝐓❨f❩ → Decidable (∃l1. @↑❨l1,f❩ ≘ l2).
+lemma is_pr_nat_dec (f) (l2): 𝐓❨f❩ → Decidable (∃l1. ＠§❨l1,f❩ ≘ l2).
 #f #l2 #Hf elim (is_pr_pat_dec … (↑l2) Hf)
 [ * /3 width=2 by ex_intro, or_introl/
 | #H @or_intror * /3 width=2 by ex_intro/