proposition: Lemma powersetU X1 X2 (X3 : {fset T}) : (X1 `|` X2 \in powerset X3) = (X1 \in powerset X3) && (X2 \in powerset X3).
proof: Proof. by rewrite !powersetE fsubUset. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)