Apply MetaCatConcrete (λX ⇒ X ∈ UnivOf (UnivOf Empty)) (λX ⇒ X) SetHom to the current goal.

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.

An exact proof term for the current goal is lam_id_exp_In X.

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

Assume HX HY HZ Hf Hg.

An exact proof term for the current goal is lam_comp_exp_In X Y Z f Hf g Hg.

∎