proposition: Lemma for_all_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 ∧ (forall 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. tauto. * rewrite IHl. split; intros [Hb Hl]. + rewrite andb_true_iff in Hb. destruct Hb as [? Hb]. split; trivial. intros x' v' Hin. inversion_clear Hin. - destruct H0 as [Heq₁ Heq₂]. hnf in Heq₁, Heq₂. simpl in Heq₁, Heq₂. rewrite Heq₁, Heq₂. assumption. - apply Hl. assumption. + subst b. simpl. split; intros; apply Hl; solve [left; reflexivity | right; assumption]. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface