Assume HC.
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.
An exact proof term for the current goal is MetaCat_IdFunctor.
∎