proposition: Lemma finverse_unique : forall f g h, are_finverse f g -> are_finverse f h -> g = h.
proof: Proof. ir. apply Umorphism.inverse_unique with f. cp H. uh H1; ee. uhg; ee. app functor_umorphism_axioms. uh H2; ee; am. uh H0; ee. uhg; ee. app functor_umorphism_axioms. uh H1; ee; am. wrr are_finverse_umorphism_inverse. uh H; ee; am. uh H; ee; am. wrr are_finverse_umorphism_inverse. uh H0; ee; am. uh H0; ee; am. Qed.
imports: Arith category