proposition: Lemma eq_sym : forall A dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t A dom₂), eq m₁ m₂ -> eq m₂ m₁.
proof: Proof. intros * Heq x. rewrite Heq. reflexivity. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface