fact: Definition forall_enumerable_by_beq_staged : R := let all := List.map (@proj1_sig _ _) (enumerate { x : A | is_true (P x) }) in List.fold_right (fun y else_case => If beq x (fst y) Then g (snd y) Else else_case) base (List.combine all (List.map f all)).
imports: Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Enumerable Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Equality