proposition: Lemma list_app_eq_app A (l l' l0 l0' : list A) : l ++ l' = l0 ++ l0' -> (exists lr, l ++ lr = l0 /\ l' = lr ++ l0') \/ (exists lr, l = l0 ++ lr /\ lr ++ l' = l0').
proof: Proof. revert l0; induction l; ins; eauto. destruct l0; ins; desf; eauto. apply IHl in H; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation