proposition: Lemma add_Inf : forall (m:t elt)(x x':key)(e e':elt), Inf (x',e') m -> ltk (x',e') (x,e) -> Inf (x',e') (add x e m).
proof: Proof. induction m. - simpl; intuition. - intros. destruct a as (x'',e''). inversion_clear H. compute in H0,H1. simpl; case (X.compare x x''); intuition. Qed.
imports: FMapInterface