proposition: Lemma fimset1 (aT rT : choiceType) (f : aT -> rT) a : [fset f x | x <- [fset a]] = [fset f a].
proof: Proof. by rewrite fimsetE fset1Es fset1E. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)