Let X, Y and f be given.

Assume HX HY.

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

Let X' and bX be given.

Assume HbX.

Apply HO Y HY (λu ⇒ Hom_struct_b (pack_b X' bX) u f → f ∈ u 0^{pack_b X' bX 0}) to the current goal.

Let Y' and bY be given.

Assume HbY.

We will prove Hom_struct_b (pack_b X' bX) (pack_b Y' bY) f → f ∈ pack_b Y' bY 0^{pack_b X' bX 0}.

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

Assume Hf: f ∈ Y'^X' ∧ (∀x x' ∈ X', f (bX x x') = bY (f x) (f x')).

Apply Hf to the current goal.

Assume Hf1 Hf2.

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

Let X' and bX be given.

Assume HbX.

We will prove Hom_struct_b (pack_b X' bX) (pack_b X' bX) (lam_id (pack_b X' bX 0)).

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

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

We will prove lam_id X' ∈ X'^X' ∧ (∀x x' ∈ X', lam_id X' (bX x x') = bX (lam_id X' x) (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.

Let x' be given.

Assume Hx'.

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

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

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

An exact proof term for the current goal is beta X' (λx ⇒ x) (bX x x') (HbX x Hx x' Hx').

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

Assume HX HY HZ.

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

Let X' and bX be given.

Assume HbX.

We will prove Hom_struct_b (pack_b X' bX) Y f → Hom_struct_b Y Z g → Hom_struct_b (pack_b X' bX) Z (lam_comp (pack_b X' bX 0) g f).

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

We will prove Hom_struct_b (pack_b X' bX) Y f → Hom_struct_b Y Z g → Hom_struct_b (pack_b X' bX) Z (lam_comp X' g f).

Apply HO Y HY (λu ⇒ Hom_struct_b (pack_b X' bX) u f → Hom_struct_b u Z g → Hom_struct_b (pack_b X' bX) Z (lam_comp X' g f)) to the current goal.

Let Y' and bY be given.

Assume HbY.

We will prove Hom_struct_b (pack_b X' bX) (pack_b Y' bY) f → Hom_struct_b (pack_b Y' bY) Z g → Hom_struct_b (pack_b X' bX) Z (lam_comp X' g f).

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

Assume Hf: f ∈ Y'^X' ∧ (∀x x' ∈ X', f (bX x x') = bY (f x) (f x')).

Apply HO Z HZ (λu ⇒ Hom_struct_b (pack_b Y' bY) u g → Hom_struct_b (pack_b X' bX) u (lam_comp X' g f)) to the current goal.

Let Z' and bZ be given.

Assume HbZ.

We will prove Hom_struct_b (pack_b Y' bY) (pack_b Z' bZ) g → Hom_struct_b (pack_b X' bX) (pack_b Z' bZ) (lam_comp X' g f).

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

Assume Hg: g ∈ Z'^Y' ∧ (∀y y' ∈ Y', g (bY y y') = bZ (g y) (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' ∈ X', lam_comp X' g f (bX x x') = bZ (lam_comp X' g f x) (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.

Let x' be given.

Assume Hx'.

We will prove lam_comp X' g f (bX x x') = bZ ((λx ∈ X' ⇒ g (f x)) x) ((λx ∈ X' ⇒ g (f x)) x').

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

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

We will prove (λx ∈ X' ⇒ g (f x)) (bX x x') = bZ (g (f x)) (g (f x')).

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

We will prove g (f (bX x x')) = bZ (g (f x)) (g (f x')).

rewrite the current goal using Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (f x') (ap_Pi X' (λ_ ⇒ Y') f x' Hf1 Hx') (from right to left).

We will prove g (f (bX x x')) = g (bY (f x) (f x')).

Use f_equal.

An exact proof term for the current goal is Hf2 x Hx x' Hx'.