proposition: Lemma cancel_postcomposition {C : precategory_data} {a b c: C} (f f' : a --> b) (g : b --> c) : f = f' -> f · g = f' · g.
proof: Proof. intro; apply maponpaths_2; assumption. Defined.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations