+(* Inversion lemmas with tail ***********************************************)
+
+lemma sor_inv_tl_sn: âf1,f2,f. ⍹f1 â f2 ⥠f â f1 â ⍯f2 ⥠⍯f.
+#f1 #f2 #f elim (pn_split f1) *
+#g1 #H destruct /2 width=7 by sor_pn, sor_nn/
+qed-.
+
+lemma sor_inv_tl_dx: âf1,f2,f. f1 â ⍹f2 ⥠f â ⍯f1 â f2 ⥠⍯f.
+#f1 #f2 #f elim (pn_split f2) *
+#g2 #H destruct /2 width=7 by sor_np, sor_nn/
+qed-.
+