Let X, Y and f be given.

Assume HX HY.

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

Let X' and CX be given.

Apply HO Y HY (λu ⇒ Hom_struct_c (pack_c X' CX) u f → f ∈ u 0^{pack_c X' CX 0}) to the current goal.

Let Y' and CY be given.

We will prove Hom_struct_c (pack_c X' CX) (pack_c Y' CY) f → f ∈ pack_c Y' CY 0^{pack_c X' CX 0}.

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

Assume Hf: f ∈ Y'^X' ∧ (∀U : set → prop, (∀y, U y → y ∈ Y') → CY U → CX (λx ⇒ x ∈ X' ∧ U (f x))).

Apply Hf to the current goal.

Assume Hf1 Hf2.

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

Let X' and CX be given.

We will prove Hom_struct_c (pack_c X' CX) (pack_c X' CX) (lam_id (pack_c X' CX 0)).

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

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

We will prove lam_id X' ∈ X'^X' ∧ (∀U : set → prop, (∀y, U y → y ∈ X') → CX U → CX (λx ⇒ x ∈ X' ∧ U (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 U be given.

Assume HU1 HU2.

We prove the intermediate claim L1: U = (λx ⇒ x ∈ X' ∧ U (lam_id X' x)).

Apply pred_ext_2 to the current goal.

Let x be given.

Assume Hx.

We will prove x ∈ X' ∧ U (lam_id X' x).

Apply andI to the current goal.

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

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

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

An exact proof term for the current goal is Hx.

Let x be given.

Assume Hx.

Apply Hx to the current goal.

Assume Hx1.

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

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

Assume Hx2.

An exact proof term for the current goal is Hx2.

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

An exact proof term for the current goal is HU2.

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

Assume HX HY HZ.

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

Let X' and CX be given.

We will prove Hom_struct_c (pack_c X' CX) Y f → Hom_struct_c Y Z g → Hom_struct_c (pack_c X' CX) Z (lam_comp (pack_c X' CX 0) g f).

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

We will prove Hom_struct_c (pack_c X' CX) Y f → Hom_struct_c Y Z g → Hom_struct_c (pack_c X' CX) Z (lam_comp X' g f).

Apply HO Y HY (λu ⇒ Hom_struct_c (pack_c X' CX) u f → Hom_struct_c u Z g → Hom_struct_c (pack_c X' CX) Z (lam_comp X' g f)) to the current goal.

Let Y' and CY be given.

We will prove Hom_struct_c (pack_c X' CX) (pack_c Y' CY) f → Hom_struct_c (pack_c Y' CY) Z g → Hom_struct_c (pack_c X' CX) Z (lam_comp X' g f).

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

Assume Hf: f ∈ Y'^X' ∧ (∀U : set → prop, (∀y, U y → y ∈ Y') → CY U → CX (λx ⇒ x ∈ X' ∧ U (f x))).

Apply HO Z HZ (λu ⇒ Hom_struct_c (pack_c Y' CY) u g → Hom_struct_c (pack_c X' CX) u (lam_comp X' g f)) to the current goal.

Let Z' and CZ be given.

We will prove Hom_struct_c (pack_c Y' CY) (pack_c Z' CZ) g → Hom_struct_c (pack_c X' CX) (pack_c Z' CZ) (lam_comp X' g f).

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

Assume Hg: g ∈ Z'^Y' ∧ (∀U : set → prop, (∀z, U z → z ∈ Z') → CZ U → CY (λy ⇒ y ∈ Y' ∧ U (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' ∧ (∀U : set → prop, (∀z, U z → z ∈ Z') → CZ U → CX (λx ⇒ x ∈ X' ∧ U (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 U be given.

Assume HU1: ∀z, U z → z ∈ Z'.

Assume HU2: CZ U.

We prove the intermediate claim L2: CY (λy ⇒ y ∈ Y' ∧ U (g y)).

An exact proof term for the current goal is Hg2 U HU1 HU2.

We prove the intermediate claim L3: ∀y, y ∈ Y' ∧ U (g y) → y ∈ Y'.

Let y be given.

An exact proof term for the current goal is andEL (y ∈ Y') (U (g y)).

We prove the intermediate claim L4: CX (λx ⇒ x ∈ X' ∧ (f x ∈ Y' ∧ U (g (f x)))).

An exact proof term for the current goal is Hf2 (λy ⇒ y ∈ Y' ∧ U (g y)) L3 L2.

We prove the intermediate claim L5: (λx : set ⇒ x ∈ X' ∧ (f x ∈ Y' ∧ U (g (f x)))) = (λx : set ⇒ x ∈ X' ∧ U (lam_comp X' g f x)).

Apply pred_ext_2 to the current goal.

Let x be given.

Assume Hx.

Apply Hx to the current goal.

Assume Hx1 Hx23.

Apply Hx23 to the current goal.

Assume Hx2 Hx3.

We will prove x ∈ X' ∧ U (lam_comp X' g f x).

Apply andI to the current goal.

An exact proof term for the current goal is Hx1.

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

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

An exact proof term for the current goal is Hx3.

Let x be given.

Assume Hx.

Apply Hx to the current goal.

Assume Hx1.

We will prove U ((λx ∈ X' ⇒ g (f x)) x) → x ∈ X' ∧ (f x ∈ Y' ∧ U (g (f x))).

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

Assume Hx2.

We will prove x ∈ X' ∧ (f x ∈ Y' ∧ U (g (f x))).

Apply andI to the current goal.

An exact proof term for the current goal is Hx1.

Apply andI to the current goal.

An exact proof term for the current goal is ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx1.

An exact proof term for the current goal is Hx2.

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

An exact proof term for the current goal is L4.