proposition: Lemma in_fimset2F (f g : aT1 -> aT2 -> T) a b : (forall a b a' b', f a b <> g a' b') -> (f a b \in fimset2 g A B = false).
proof: Proof. move => H. apply/negbTE. apply/negP. by case/fimset2P => ? ? /H. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)