+lemma lsubf_beta_tl_dx: ∀f,f0,g1,L1,V. L1 ⊢ 𝐅*⦃V⦄ ≘ f → f0 ⋓ f ≘ g1 →
+ ∀f2,L2,W. ⦃L1, f0⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
+ ∃∃f1. ⦃L1.ⓓⓝW.V, f1⦄ ⫃𝐅* ⦃L2.ⓛW, f2⦄ & ⫱f1 ⊆ g1.
+#f #f0 #g1 #L1 #V #Hf #Hg1 #f2
+elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
+[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
+| @(ex2_intro … (↑g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
+]
+qed-.
+
+(* Note: this might be moved *)