update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
index ca6a8d5acedb1dd104b26ff6d78195462906dd75..3ca8053d8cf0e9353c406c884fb3b112f50ac8ba 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/pr_eq.ma".
+include "ground/relocation/pr_tl_eq.ma".
 include "ground/relocation/pr_nexts.ma".
 
 (* ITERATED NEXT FOR PARTIAL RELOCATION MAPS ********************************)
@@ -25,3 +25,24 @@ lemma pr_nexts_eq_repl (n):
 #n @(nat_ind_succ … n) -n
 /3 width=5 by pr_eq_next/
 qed.
+
+(* Inversions with pr_eq ****************************************************)
+
+lemma pr_eq_inv_nexts_push_bi (f1) (f2) (n1) (n2):
+      ↑*[n1] ⫯f1 ≡ ↑*[n2] ⫯f2 →
+      ∧∧ n1 = n2 & f1 ≡ f2.
+#f1 #f2
+#n1 @(nat_ind_succ … n1) -n1 [| #n1 #IH ]
+#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
+[ <pr_nexts_zero <pr_nexts_succ #H
+  elim (pr_eq_inv_push_next … H) -H //
+| <pr_nexts_succ <pr_nexts_succ #H
+  lapply (pr_eq_inv_next_bi … H ????) -H [5:|*: // ] #H
+  elim (IH … H) -IH -H /2 width=1 by conj/
+| <pr_nexts_zero <pr_nexts_zero #H
+  lapply (pr_eq_inv_push_bi … H ????) -H [5:|*: // ] #H
+  /2 width=1 by conj/
+| <pr_nexts_succ <pr_nexts_zero #H
+  elim (pr_eq_inv_next_push … H) -H //
+]
+qed-.