proposition: Lemma find_eq : forall m (Hm:NoDupA m) x x', X.eq x x' -> find x m = find x' m.
proof: Proof. induction m; simpl; auto; destruct a; intros. inversion_clear Hm. rewrite (IHm H1 x x'); auto. destruct (X.eq_dec x t0) as [|Hneq]; destruct (X.eq_dec x' t0) as [|?Hneq']; trivial. - elim Hneq'; apply X.eq_trans with x; auto. - elim Hneq; apply X.eq_trans with x'; auto. Qed.
imports: FMapInterface