proposition: Lemma remove_id_right (C : precategory) (a b : C) (f g : a --> b) (h : b --> b): h = identity _ -> f = g -> f · h = g.
proof: Proof. intros H eq. intermediate_path (f · identity _). - destruct H. apply idpath. - intermediate_path f. + apply id_right. + apply eq. Defined.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations