proposition: Lemma forall_enumerable_by_beq_correct : forall_enumerable_by_beq = if P x then f x else base.
proof: Proof. unfold forall_enumerable_by_beq. destruct Henum as [ls Hls]; clear Henum; simpl. specialize (fun p => Hls (exist _ x p)); simpl in Hls. case_eq (P x); intro Heq; [ specialize (Hls Heq) | clear Hls ]. { induction ls as [|k ks IHks]; simpl in *; destruct_head False; destruct Hls as [Hls|Hls]; specialize_by assumption; subst; simpl in *. { rewrite lb by reflexivity; simpl; reflexivity. } { rewrite IHks. destruct (beq x (proj1_sig k)) eqn:Heq'; simpl; trivial. apply bl in Heq'; subst; reflexivity. } } { induction ls as [|k ks IHks]; simpl in *. { reflexivity. } { rewrite IHks. destruct (beq x (proj1_sig k)) eqn:Heq'; simpl; trivial. apply bl in Heq'; subst x. destruct k; simpl in *; congruence. } } Qed.
imports: Fiat.Common Fiat.Common.Enumerable Fiat.Common.Equality