proposition: Lemma union_right : forall {A: Type} (x: A) (seq1 seq2: list A), SetEq (SetUnion seq1 (x::seq2)) (x :: (SetUnion seq1 seq2)).
proof: Proof. intros; unfold SetEq, SetUnion; intuition; repeat (rewrite in_app_iff in *; simpl in *); intuition. Qed.
imports: Coq.Lists.List Coq.Bool.Bool Coq.Structures.OrderedType Coq.Classes.Morphisms Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat