proposition: Lemma find_eq : forall m (Hm:Ok m) x x', K.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. dec; dec; trivial. elim E0. now transitivity x. elim E. now transitivity x'. Qed.
imports: Coq(EqualitiesFacts)