proposition: Lemma Sfind_compat : forall {A x y} {m : S.t A}, X.eq x y -> S.find x m = S.find y m.
proof: Proof. intros A x y m Hxy. destruct (S.find y m) eqn:Hin. + symmetry in Hxy. eapply S.find_1, S.MapsTo_1, S.find_2; eassumption. + destruct (S.find x m) eqn:Habs; trivial. rewrite <- Hin. symmetry. eapply S.find_1, S.MapsTo_1, S.find_2; eassumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface