proposition: Lemma fimset3P x : reflect (fimset3_spec x) (x \in [fset f a b c | a <- A , b <- B , c <- C]).
proof: Proof. apply: (iffP (fimset2P _ _ _ _)) => [[a [b c] /= ? ? ] | [a b c -> H H1 H2] ]. - rewrite in_fsetX => /andP [? ?]. exact: fImset3_spec. - apply: (@fImset_spec _ _ _ _ _ _ _ _ (b,c)) H _ => //. by rewrite in_fsetX H1 H2. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)