proposition: Lemma fimset2P (rT : choiceType) f (y : rT) : reflect (fimset2_spec f y) (y \in fimset2 f A B).
proof: Proof. rewrite fimset2E set_ofE. apply: (iffP allpairsP). case => [[a b] /= [? ? ?]]. exact: fImset_spec. case => a b *. exists (a,b). by split. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)