Let X, Y and f be given.

Assume HX HY.

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

Let X' and pX be given.

Apply HO Y HY (λu ⇒ Hom_struct_p (pack_p X' pX) u f → f ∈ u 0^{pack_p X' pX 0}) to the current goal.

Let Y' and pY be given.

We will prove Hom_struct_p (pack_p X' pX) (pack_p Y' pY) f → f ∈ pack_p Y' pY 0^{pack_p X' pX 0}.

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

Assume Hf: f ∈ Y'^X' ∧ (∀x ∈ X', pX x → pY (f x)).

Apply Hf to the current goal.

Assume Hf1 Hf2.

rewrite the current goal using pack_p_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_p u u (lam_id (u 0))) to the current goal.

Let X' and pX be given.

We will prove Hom_struct_p (pack_p X' pX) (pack_p X' pX) (lam_id (pack_p X' pX 0)).

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

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

We will prove lam_id X' ∈ X'^X' ∧ (∀x ∈ X', pX x → pX (lam_id X' x)).

Apply andI to the current goal.

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

Let x be given.

Assume Hx Hx2.

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

rewrite the current goal using beta X' (λx ⇒ x) x Hx (from left to right).

An exact proof term for the current goal is Hx2.

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

Assume HX HY HZ.

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

Let X' and pX be given.

We will prove Hom_struct_p (pack_p X' pX) Y f → Hom_struct_p Y Z g → Hom_struct_p (pack_p X' pX) Z (lam_comp (pack_p X' pX 0) g f).

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

We will prove Hom_struct_p (pack_p X' pX) Y f → Hom_struct_p Y Z g → Hom_struct_p (pack_p X' pX) Z (lam_comp X' g f).

Apply HO Y HY (λu ⇒ Hom_struct_p (pack_p X' pX) u f → Hom_struct_p u Z g → Hom_struct_p (pack_p X' pX) Z (lam_comp X' g f)) to the current goal.

Let Y' and pY be given.

We will prove Hom_struct_p (pack_p X' pX) (pack_p Y' pY) f → Hom_struct_p (pack_p Y' pY) Z g → Hom_struct_p (pack_p X' pX) Z (lam_comp X' g f).

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

Assume Hf: f ∈ Y'^X' ∧ (∀x ∈ X', pX x → pY (f x)).

Apply HO Z HZ (λu ⇒ Hom_struct_p (pack_p Y' pY) u g → Hom_struct_p (pack_p X' pX) u (lam_comp X' g f)) to the current goal.

Let Z' and pZ be given.

We will prove Hom_struct_p (pack_p Y' pY) (pack_p Z' pZ) g → Hom_struct_p (pack_p X' pX) (pack_p Z' pZ) (lam_comp X' g f).

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

Assume Hg: g ∈ Z'^Y' ∧ (∀y ∈ Y', pY y → pZ (g y)).

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' ∧ (∀x ∈ X', pX x → pZ (lam_comp X' g f x)).

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.

Let x be given.

Assume Hx Hx2.

We will prove pZ ((λx ∈ X' ⇒ g (f x)) x).

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

We will prove pZ (g (f x)).

Apply Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) to the current goal.

Apply Hf2 x Hx to the current goal.

An exact proof term for the current goal is Hx2.