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