proposition: Lemma setU_comm {U} (s1 s2 : set U) : s1 :|: s2 <--> s2 :|: s1.
proof: Proof. firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)