proposition: Lemma remove_1 : forall m (Hm:NoDupA m) x y, X.eq x y -> ~ In y (remove x m).
proof: Proof. induction m as [|[a m]]; intros Hm x y H; simpl in *. - inversion 1; inversion H1. - inversion_clear Hm. destruct X.eq_dec. + intros [e' ?]; elim H0. apply InA_eqk with (y, e'). * apply X.eq_trans with x; [|auto]. apply X.eq_sym; auto. * apply InA_eqke_eqk; auto. + intros [e' H2]; apply InA_cons in H2; destruct H2. * elim n; apply X.eq_trans with y; [auto|apply H2]. * elim IHm with x y; auto. exists e'; auto. Qed.
imports: FMapInterface