Let X, Y and f be given.

Assume HX HY.

Apply HO X HX (λu ⇒ Hom_struct_e u Y f → f ∈ Y 0^{u 0}) to the current goal.

Let X' and eX be given.

Assume HeX.

Apply HO Y HY (λu ⇒ Hom_struct_e (pack_e X' eX) u f → f ∈ u 0^{pack_e X' eX 0}) to the current goal.

Let Y' and eY be given.

Assume HeY.

We will prove Hom_struct_e (pack_e X' eX) (pack_e Y' eY) f → f ∈ pack_e Y' eY 0^{pack_e X' eX 0}.

rewrite the current goal using Hom_struct_e_pack (from left to right).

Assume Hf: f ∈ Y'^X' ∧ f eX = eY.

Apply Hf to the current goal.

Assume Hf1 Hf2.

rewrite the current goal using pack_e_0_eq2 (from right to left).

An exact proof term for the current goal is Hf1.

Let X be given.

Assume HX.

Apply HO X HX (λu ⇒ Hom_struct_e u u (lam_id (u 0))) to the current goal.

Let X' and eX be given.

Assume HeX.

We will prove Hom_struct_e (pack_e X' eX) (pack_e X' eX) (lam_id (pack_e X' eX 0)).

rewrite the current goal using pack_e_0_eq2 (from right to left).

rewrite the current goal using Hom_struct_e_pack (from left to right).

We will prove lam_id X' ∈ X'^X' ∧ lam_id X' eX = eX.

Apply andI to the current goal.

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

We will prove (λx ∈ X' ⇒ x) eX = eX.

An exact proof term for the current goal is beta X' (λx ⇒ x) eX HeX.

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

Assume HX HY HZ.

Apply HO X HX (λu ⇒ Hom_struct_e u Y f → Hom_struct_e Y Z g → Hom_struct_e u Z (lam_comp (u 0) g f)) to the current goal.

Let X' and eX be given.

Assume HeX.

We will prove Hom_struct_e (pack_e X' eX) Y f → Hom_struct_e Y Z g → Hom_struct_e (pack_e X' eX) Z (lam_comp (pack_e X' eX 0) g f).

rewrite the current goal using pack_e_0_eq2 (from right to left).

We will prove Hom_struct_e (pack_e X' eX) Y f → Hom_struct_e Y Z g → Hom_struct_e (pack_e X' eX) Z (lam_comp X' g f).

Apply HO Y HY (λu ⇒ Hom_struct_e (pack_e X' eX) u f → Hom_struct_e u Z g → Hom_struct_e (pack_e X' eX) Z (lam_comp X' g f)) to the current goal.

Let Y' and eY be given.

Assume HeY.

We will prove Hom_struct_e (pack_e X' eX) (pack_e Y' eY) f → Hom_struct_e (pack_e Y' eY) Z g → Hom_struct_e (pack_e X' eX) Z (lam_comp X' g f).

rewrite the current goal using Hom_struct_e_pack (from left to right).

Assume Hf: f ∈ Y'^X' ∧ f eX = eY.

Apply HO Z HZ (λu ⇒ Hom_struct_e (pack_e Y' eY) u g → Hom_struct_e (pack_e X' eX) u (lam_comp X' g f)) to the current goal.

Let Z' and eZ be given.

Assume HeZ.

We will prove Hom_struct_e (pack_e Y' eY) (pack_e Z' eZ) g → Hom_struct_e (pack_e X' eX) (pack_e Z' eZ) (lam_comp X' g f).

rewrite the current goal using Hom_struct_e_pack (from left to right).

Assume Hg: g ∈ Z'^Y' ∧ g eY = eZ.

Apply Hf to the current goal.

Assume Hf1 Hf2.

Apply Hg to the current goal.

Assume Hg1 Hg2.

We will prove lam_comp X' g f ∈ Z'^X' ∧ lam_comp X' g f eX = eZ.

Apply andI to the current goal.

An exact proof term for the current goal is lam_comp_exp_In X' Y' Z' f Hf1 g Hg1.

We will prove (λx ∈ X' ⇒ g (f x)) eX = eZ.

rewrite the current goal using beta X' (λx ⇒ g (f x)) eX HeX (from left to right).

We will prove g (f eX) = eZ.

rewrite the current goal using Hf2 (from left to right).

An exact proof term for the current goal is Hg2.