Assume H1 H2 H3.

Apply MetaCat_I to the current goal.

An exact proof term for the current goal is H2.

An exact proof term for the current goal is H3.

Let X, Y and f be given.

Assume HX HY Hf.

We will prove lam_comp (U X) f (lam_id (U X)) = f.

An exact proof term for the current goal is lam_comp_id_R (U X) (U Y) f (H1 X Y f HX HY Hf).

Let X, Y and f be given.

Assume HX HY Hf.

We will prove lam_comp (U X) (lam_id (U Y)) f = f.

An exact proof term for the current goal is lam_comp_id_L (U X) (U Y) f (H1 X Y f HX HY Hf).

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

Assume HX HY HZ HW Hf Hg Hh.

Use symmetry.

An exact proof term for the current goal is lam_comp_assoc (U X) (U Y) f (H1 X Y f HX HY Hf) g h.

∎