fact: CoInductive fimset2_spec (rT : choiceType) f (y : rT) : Prop := fImset_spec a b : y = f a b -> a \in A -> b \in B -> fimset2_spec f y.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)