proposition: Lemma mem_fimset2 (rT : choiceType) (f : aT1 -> aT2 -> rT) a b : a \in A -> b \in B -> f a b \in fimset2 f A B.
proof: Proof. move => inA inB. apply/fimset2P. exact: fImset_spec. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)