proposition: Lemma in_fimset2 (f : aT1 -> aT2 -> T) a b : injective2 f -> (f a b \in fimset2 f A B) = (a \in A) && (b \in B).
proof: Proof. move => f_inj. apply/idP/idP; last by case/andP; exact: mem_fimset2. case/fimset2P => a' b' /f_inj [-> ->]. by bcase. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)