Lemma pre_comp_with_z_iso_is_inj' {C : precategory} {a b b' : C} {f : a --> b} (i : is_z_isomorphism f) : ∏ (f' g' : b --> b'), f · f' = f · g' -> f' = g'. Proof. intros f' g' H. apply (pre_comp_with_z_iso_is_inj (pr2 i)). exact H. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories.