An exact proof term for the current goal is and4E (∀X, Obj X → Obj' (F0 X)) (∀X Y f, Obj X → Obj Y → Hom X Y f → Hom' (F0 X) (F0 Y) (F1 X Y f)) (∀X, Obj X → F1 X X (id X) = id' (F0 X)) (∀X Y Z f g, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → F1 X Z (comp X Y Z g f) = comp' (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f)).