proposition: Lemma forall_enumerable_by_beq_aggregate_correct_reachable (H : is_true (P x)) : forall_enumerable_by_beq_aggregate = g (f x).
proof: Proof. rewrite forall_enumerable_by_beq_aggregate_correct, H by (rewrite H; reflexivity). reflexivity. Qed.
imports: Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Enumerable Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Equality