proposition: Lemma add_InA : forall m x y e e', ~ K.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m.
proof: Proof. induction m as [ | (k,e') m IH]; simpl; intros. - inversion_clear H0. elim H. symmetry; apply H1. inversion_clear H1. - revert H0; dec; rewrite !InA_cons. + rewrite E. intuition. + intuition. right; eapply IH; eauto. Qed.
imports: Coq(EqualitiesFacts)