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