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