proposition: Lemma Aphi_invPres : forall f g : d --> G c, f =_S g -> ApAphi_inv f =_S ApAphi_inv g.
proof: Proof. intros; unfold ApAphi_inv in |- *; apply (Pres (NatIso_inv ad (Build_POb1 d c))); assumption. Qed.
imports: NatIso HomFunctor2