]
qed-.
+lemma eq_inv_list_append_empty (A):
+ ∀l1,l2. l1⨁{A}l2 = ⓔ →
+ ∧∧ l1 = ⓔ & l2 = ⓔ.
+#A *
+[ #l2 /2 width=1 by conj/
+| #a1 #l1 #l2 <list_append_lcons_sn #H destruct
+]
+qed-.
+
(* Advanced inversions ******************************************************)
lemma eq_inv_list_append_dx_sn_refl (A) (l1) (l2):