proposition: Lemma app_eq_cons A (l1 l2 : list A) a l : l1 ++ l2 = a :: l <-> (l1 = nil /\ l2 = a :: l) \/ (exists l1', l1 = a :: l1' /\ l1' ++ l2 = l).
proof: Proof. split; ins; desf. destruct l1; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation