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