proposition: Lemma PsetsU s1 s2 E : s1 \in Psets E -> s2 \in Psets E -> s1 :|: s2 \in Psets E.
proof: Proof. rewrite /Psets. rewrite inE; case/andP => s1E Ps1. rewrite inE; case/andP => s2E Ps2. rewrite inE. apply/andP; split. by apply/subUsetP. by rewrite PU. Qed.
imports: mathcomp(all_ssreflect)