proposition: Lemma exists_spec_aux : forall dom A f, Proper (X.eq ==> Logic.eq ==> Logic.eq) f -> forall (m : t A dom) l b, fold_left (fun acc xv => acc || f (fst xv) (snd xv)) l b = true <-> b = true ∨ (exists x (v : A), InA (X.eq * Logic.eq)%signature (x, v) l ∧ f x v = true).
proof: Proof. intros dom A f Hf m l. induction l as [| [x v] l]; intro b; simpl. * setoid_rewrite InA_nil. firstorder. * rewrite IHl. split; intros [Hb | Hl]. + rewrite orb_true_iff in Hb. destruct Hb as [Hb | Hb]. - now left. - right. exists x, v. split; trivial. now left. + destruct Hl as [x' [v' [Hl Hfx]]]. right. exists x', v'. split; trivial. now right. + subst b. now left. + destruct Hl as [x' [v' [Hl Hfx]]]. inversion_clear Hl. - left. destruct H as [Heq₁ Heq₂]. hnf in Heq₁, Heq₂. simpl in Heq₁, Heq₂. rewrite Heq₁, Heq₂ in Hfx. rewrite Hfx. apply orb_b_true. - right. exists x', v'. split; trivial. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface