X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts.ma;h=1b383569934c5ff49afe90c9b24b45705b723590;hp=b888af22d7fa684c8226547d410179a0627c3356;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hpb=f38fd769279794d0ca73c8945eac30e8b42e59be

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index b888af22d..1b3835699 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -287,6 +287,22 @@ lemma lifts_inv_pair_xy_y: ∀I,T,V,f. ⇧*[f] ②{I}V.T ≘ T → ⊥.
 ]
 qed-.
 
+lemma lifts_inv_push_zero_sn (f):
+      ∀X. ⇧*[⫯f]#0 ≘ X → #0 = X.
+#f #X #H
+elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct
+lapply (at_inv_ppx … Hi ???) -Hi //
+qed-.
+
+lemma lifts_inv_push_succ_sn (f) (i1):
+      ∀X. ⇧*[⫯f]#(↑i1) ≘ X →
+      ∃∃i2. ⇧*[f]#i1 ≘ #i2 & #(↑i2) = X.
+#f #i1 #X #H
+elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
+elim (at_inv_npx … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
+/3 width=3 by lifts_lref, ex2_intro/
+qed-.
+
 (* Inversion lemmas with uniform relocations ********************************)
 
 lemma lifts_inv_lref1_uni: ∀l,Y,i. ⇧*[l] #i ≘ Y → Y = #(l+i).