proposition: Lemma find_find : forall m m' x, find x m = find x m' <-> (forall d, find x m = Some d <-> find x m' = Some d).
proof: Proof. intros; destruct (find x m); destruct (find x m'); split; intros; try split; try congruence. - rewrite H; auto. - symmetry; rewrite <- H; auto. - rewrite H; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int