proposition: Lemma eq_dom : forall A dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t A dom₂), eq m₁ m₂ -> Dom.eq dom₁ dom₂.
proof: Proof. intros * Heq ?. do 2 rewrite <- S.find_spec. setoid_rewrite Heq. reflexivity. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface