Assume HF HG.

Apply MetaFunctor_strict_E Obj Hom id comp Obj' Hom' id' comp' F0 F1 HF to the current goal.

Assume HC _ HF.

Apply MetaFunctor_strict_E Obj' Hom' id' comp' Obj'' Hom'' id'' comp'' G0 G1 HG to the current goal.

Assume _ HC'' HG.

Apply MetaFunctor_strict_I to the current goal.

An exact proof term for the current goal is HC.

An exact proof term for the current goal is HC''.

Apply MetaCat_CompFunctors to the current goal.

An exact proof term for the current goal is HF.

An exact proof term for the current goal is HG.

∎