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