proposition: Lemma Equal_hom_trans : f =_H g -> g =_H h -> f =_H h.
proof: Proof. intros eqdep_fg. elim eqdep_fg; intros k eq_fk eqdep_kh. elim eqdep_kh; intros l eq_kl. apply Build_Equal_hom. apply Trans with k; auto. Qed.
imports: Category