X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_map.ma;h=b50b08175b291da461c487ce6f757483ef116ca3;hb=9709aaeb059e24359d5d8a3997ef22974bff3718;hp=80a67e3201ebde0eb0cebb919e3c38861f0fec4a;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma
index 80a67e320..b50b08175 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma
@@ -40,3 +40,49 @@ qed.
 lemma tr_inj_unfold_succ (f): ∀p. ↑𝐭❨p⨮f❩ = 𝐭❨↑p⨮f❩.
 #f #p <(stream_unfold … (𝐭❨↑p⨮f❩)) in ⊢ (???%); //
 qed.
+
+(* Basic inversions *********************************************************)
+
+(*** push_inv_seq_sn *)
+lemma eq_inv_cons_pr_push (f) (g):
+      ∀p. 𝐭❨p⨮g❩ = ⫯f → ∧∧ 𝟏 = p & 𝐭❨g❩ = f.
+#f #g *
+[ <tr_inj_unfold_unit
+  /3 width=1 by eq_inv_pr_push_bi, conj/
+| #p <tr_inj_unfold_succ #H
+  elim (eq_inv_pr_next_push … H)
+]
+qed-.
+
+(*** push_inv_seq_dx *)
+lemma eq_inv_pr_push_cons (f) (g):
+      ∀p. ⫯f = 𝐭❨p⨮g❩ → ∧∧ 𝟏 = p & 𝐭❨g❩ = f.
+#f #g *
+[ <tr_inj_unfold_unit
+  /3 width=1 by eq_inv_pr_push_bi, conj/
+| #p <tr_inj_unfold_succ #H
+  elim (eq_inv_pr_push_next … H)
+]
+qed-.
+
+(*** next_inv_seq_sn *)
+lemma eq_inv_cons_pr_next (f) (g):
+      ∀p. 𝐭❨p⨮g❩ = ↑f → ∃∃q. 𝐭❨q⨮g❩ = f & ↑q = p.
+#f #g *
+[ <tr_inj_unfold_unit #H
+  elim (eq_inv_pr_push_next … H)
+| #p <tr_inj_unfold_succ #H
+  /3 width=3 by eq_inv_pr_next_bi, ex2_intro/
+]
+qed-.
+
+(*** next_inv_seq_dx *)
+lemma eq_inv_pr_next_cons (f) (g):
+      ∀p. ↑f = 𝐭❨p⨮g❩ → ∃∃q. 𝐭❨q⨮g❩ = f & ↑q = p.
+#f #g *
+[ <tr_inj_unfold_unit #H
+  elim (eq_inv_pr_next_push … H)
+| #p <tr_inj_unfold_succ #H
+  /3 width=3 by eq_inv_pr_next_bi, ex2_intro/
+]
+qed-.