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