proposition: Lemma Adj_eq6 : ApAphi_inv ad (h o g) =_S FMor F h o ApAphi_inv ad g.
proof: Proof. apply Trans with (ApAphi_inv ad ((h o g) o FMor G (Id c))). apply Aphi_invPres. apply Trans with ((h o g) o Id (G c)). apply Idr. apply Comp_l. apply FId1. apply Trans with ((FMor F h o ApAphi_inv ad g) o Id c). apply (Adj_eq2 ad h (Id c) g). apply Idr1. Qed.
imports: NatIso HomFunctor2