partial update in static_2

[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 1d76991d1dc3d5af74e15cb6f6894977304e98a9..0b4a769f84859c0381e4516d5533ba21836d27ab 100644 (file)
--- 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 ***************************)
@@ -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-.