fact: Definition forall_enumerable_by_beq : R := List.fold_right (fun y else_case => If beq x y Then f y Else else_case) base (List.map (@proj1_sig _ _) (enumerate { x : A | is_true (P x) })).
imports: Fiat.Common Fiat.Common.Enumerable Fiat.Common.Equality