proposition: Lemma bigAUA (T : finType) (pS : pSystem) (A B : {set T}) (F : T -> pS) : mprv ((\and_(s \in A :|: B) F s) ---> (\and_(s \in A) F s) :/\: (\and_(s \in B) F s)).
proof: Proof. apply: rAI; apply: and_sub => x; by rewrite !mem_enum inE => ->. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions