Apply MetaFunctorI to the current goal.

Let X be given.

Assume HX.

An exact proof term for the current goal is HX.

Let X, Y and f be given.

Assume HX HY Hf.

An exact proof term for the current goal is Hf.

Let X be given.

Assume HX.

Use reflexivity.

Let X, Y, Z, f and g be given.

Assume HX HY HZ Hf Hg.

Use reflexivity.

∎