An exact proof term for the current goal is and3E (MetaCat Obj Hom id comp) (MetaCat Obj' Hom' id' comp') MetaFunctor.