proposition: Lemma fold_keys_ok f l : NoDupA K.eq l -> Ok (fold_keys f l).
proof: Proof. induction 1; simpl. - constructor. - destruct (f x); trivial. constructor; trivial. contradict H. apply InA_alt in H. destruct H as ((k,e'),(E,H)). rewrite fold_keys_In in H. apply InA_alt. exists k. now split. Qed.
imports: Coq(EqualitiesFacts)