An exact proof term for the current goal is andI (∀X, Obj X → Hom' (F0 X) (G0 X) (eta X)) (∀X Y f, Obj X → Obj Y → Hom X Y f → comp' (F0 X) (G0 X) (G0 Y) (G1 X Y f) (eta X) = comp' (F0 X) (F0 Y) (G0 Y) (eta Y) (F1 X Y f)).