proposition: Lemma SetEq_Symmetric : forall {A: Type}, forall (x y: list A), SetEq x y -> SetEq y x.
proof: Proof. unfold Symmetric, SetEq; intuition; autospecialize; 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