proposition: Lemma forall_enumerable_by_beq_staged_correct (H_f_good : forall y, f x = f y -> P y -> P x) : forall_enumerable_by_beq_staged = if P x then g (f x) else base.
proof: Proof. rewrite <- (forall_enumerable_by_beq_correct P x (fun y => g (f y)) base). unfold forall_enumerable_by_beq_staged, forall_enumerable_by_beq. rewrite combine_map_r, map_combine_id; simpl. rewrite fold_right_map; unfold compose; simpl. reflexivity. Qed.
imports: Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Enumerable Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Equality