+lemma lifts_inv_push_zero_sn (f):
+ ∀X. ⇧*[⫯f]#𝟎 ≘ X → #(𝟎) = X.
+#f #X #H
+elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct
+lapply (pr_pat_inv_unit_push … 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 (pr_nat_inv_succ_push … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
+/3 width=3 by lifts_lref, ex2_intro/
+qed-.
+