proposition: Lemma snoc_eq_snoc A (a a' : A) l l' : l ++ a :: nil = l' ++ a' :: nil <-> l = l' /\ a = a'.
proof: Proof. by split; ins; desf; apply app_inj_tail. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation