proposition: Lemma in_fsetX a b : ((a,b) \in A `x` B) = (a \in A) && (b \in B).
proof: Proof. apply/fimset2P/idP => [[? ? [-> ->] -> ->] //|/andP []]. exact: fImset_spec. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)