An exact proof term for the current goal is and5E (MetaFunctor_strict Obj Hom id comp Obj' Hom' id' comp' F0 F1) (MetaFunctor Obj' Hom' id' comp' Obj Hom id comp G0 G1) (MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta) (MetaNatTrans Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) eps) MetaAdjunction.