An exact proof term for the current goal is and5E (MetaCat Obj Hom id comp) (MetaCat Obj' Hom' id' comp') (MetaFunctor Obj Hom id comp Obj' Hom' id' comp' F0 F1) (MetaFunctor Obj Hom id comp Obj' Hom' id' comp' G0 G1) MetaNatTrans H.