proposition: Lemma fold_keys_In f l x e : List.In (x,e) (fold_keys f l) <-> List.In x l /\ f x = Some e.
proof: Proof. induction l as [|k l IH]; simpl. - intuition. - destruct (f k) eqn:F; simpl; rewrite IH; clear IH; intuition; try left; congruence. Qed.
imports: Coq(EqualitiesFacts)