proposition: Lemma Equiv_find_None : forall m m', Equiv eq m m' -> forall k, find k m = None <-> find k m' = None.
proof: Proof. intros m m' [h1 h2] k. split; intro hk. case_eq (find k m'); intros. 2: refl. destruct (Equiv_find_Some' (conj h1 h2) H). destruct H0. rewrite hk in H0. discr. case_eq (find k m); intros. 2: refl. destruct (Equiv_find_Some (conj h1 h2) H). destruct H0. rewrite hk in H0. discr. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)