proposition: Lemma mem_fimset3 a b c: a \in A -> b \in B -> c \in C -> f a b c \in fimset3 f A B C.
proof: Proof. move => H1 H2 H3. apply/fimset3P. exact: fImset3_spec. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)