proposition: Lemma remove_InA : forall m (Hm:Ok m) x y e, InA eqk (y,e) (remove x m) -> InA eqk (y,e) m.
proof: Proof. induction m as [ | (k,e') m IH]; simpl; trivial; intros. inversion_clear Hm. revert H; dec; rewrite !InA_cons; intuition. right; eapply H; eauto. Qed.
imports: Coq(EqualitiesFacts)