proposition: Lemma app_cons_eq_snoc A (l1 l2 : list A) a a' l : l1 ++ a :: l2 = l ++ a' :: nil <-> (l1 = l /\ a = a' /\ l2 = nil) \/ (exists l2', l2 = l2' ++ a' :: nil /\ l1 ++ a :: l2' = l).
proof: Proof. split; ins; desf; [|by rewrite <- app_assoc]. rewrite app_eq_snoc in H; ins; desf. symmetry in H; rewrite app_cons_eq_cons in H; desf; eauto using app_nil_end. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation