X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_ist_ist.ma;h=cfb786adcdc7e9880381f69e224489ed2ef8633e;hb=742e21da086654af82f308027250d00b50d67f52;hp=1d76991d1dc3d5af74e15cb6f6894977304e98a9;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

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 1d76991d1..cfb786adc 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -15,6 +15,7 @@
 include "ground/relocation/pr_eq.ma".
 include "ground/relocation/pr_pat_lt.ma".
 include "ground/relocation/pr_pat_pat.ma".
+include "ground/relocation/pr_nat.ma".
 include "ground/relocation/pr_ist.ma".
 
 (* TOTALITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************)
@@ -22,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/
@@ -31,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
@@ -44,8 +45,8 @@ qed-.
 (* Main destructions with pr_pat ********************************************)
 
 (*** at_ext *)
-corec theorem pr_eq_ext_pat (f1) (f2): 𝐓❪f1❫ → 𝐓❪f2❫ →
-              (∀i,i1,i2. @❪i,f1❫ ≘ i1 → @❪i,f2❫ ≘ i2 → i1 = i2) →
+corec theorem pr_eq_ext_pat (f1) (f2): 𝐓❨f1❩ → 𝐓❨f2❩ →
+              (∀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
@@ -66,3 +67,12 @@ cases (pr_map_split_tl f2) #H2
   lapply (Hi i (↑i1) (↑i2) ??) /2 width=5 by pr_pat_next/
 ]
 qed-.
+
+(* Advanced constructions with pr_nat ***************************************)
+
+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/
+]
+qed-.