proposition: Theorem find_compat : forall A x y dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t A dom₂), X.eq x y -> eq m₁ m₂ -> find x m₁ = find y m₂.
proof: Proof. intros * Hxy Heq. rewrite Heq. apply find_elt_compat. assumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface