proposition: Lemma andU (T : choiceType) (pS : pSystem) (F : T -> pS) (X Y : {fset T}) : mprv ((\and_(s <- X `|` Y) F s) <--> (\and_(s <- X) F s) :/\: (\and_(s <- Y) F s)).
proof: Proof. rule axAI. - apply: rAI; apply: and_sub; apply/subP; auto with fset. - apply: bigAI => s; case/fsetUP; [rewrite -> axAEl|rewrite -> axAEr]; exact: bigAE. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions