proposition: Lemma Equal_Discr_mor_equiv : Equivalence Equal_Discr_mor.
proof: Proof. unfold Equal_Discr_mor in |- *. apply Build_Equivalence; [ trivial | apply Build_Partial_equivalence ]; red in |- *; trivial. Qed.
imports: Category