definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in