proposition: Lemma Equal_MonMor_equiv : Equivalence Equal_MonMor.
proof: Proof. apply Build_Equivalence. unfold Reflexive, Equal_MonMor in |- *; intro f. unfold Ext in |- *; intros x; apply Refl. apply Build_Partial_equivalence. unfold Transitive, Equal_MonMor in |- *; intros f g h H1 H2. unfold Ext in |- *; intros x. apply Trans with (g x). apply (H1 x). apply (H2 x). unfold Symmetric, Equal_MonMor in |- *; intros f g H1. unfold Ext in |- *; intros x. apply Sym. apply (H1 x). Qed.
imports: Map2