Let X, Y and f be given.

Assume HX HY.

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

Let X' and rX be given.

Apply HO Y HY (λu ⇒ Hom_struct_r (pack_r X' rX) u f → f ∈ u 0^{pack_r X' rX 0}) to the current goal.

Let Y' and rY be given.

We will prove Hom_struct_r (pack_r X' rX) (pack_r Y' rY) f → f ∈ pack_r Y' rY 0^{pack_r X' rX 0}.

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

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

Apply Hf to the current goal.

Assume Hf1 Hf2.

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

Let X' and rX be given.

We will prove Hom_struct_r (pack_r X' rX) (pack_r X' rX) (lam_id (pack_r X' rX 0)).

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

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

We will prove lam_id X' ∈ X'^X' ∧ (∀x x' ∈ X', rX x x' → rX (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' Hx2.

We will prove rX ((λ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 Hx2.

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

Assume HX HY HZ.

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

Let X' and rX be given.

We will prove Hom_struct_r (pack_r X' rX) Y f → Hom_struct_r Y Z g → Hom_struct_r (pack_r X' rX) Z (lam_comp (pack_r X' rX 0) g f).

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

We will prove Hom_struct_r (pack_r X' rX) Y f → Hom_struct_r Y Z g → Hom_struct_r (pack_r X' rX) Z (lam_comp X' g f).

Apply HO Y HY (λu ⇒ Hom_struct_r (pack_r X' rX) u f → Hom_struct_r u Z g → Hom_struct_r (pack_r X' rX) Z (lam_comp X' g f)) to the current goal.

Let Y' and rY be given.

We will prove Hom_struct_r (pack_r X' rX) (pack_r Y' rY) f → Hom_struct_r (pack_r Y' rY) Z g → Hom_struct_r (pack_r X' rX) Z (lam_comp X' g f).

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

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

Apply HO Z HZ (λu ⇒ Hom_struct_r (pack_r Y' rY) u g → Hom_struct_r (pack_r X' rX) u (lam_comp X' g f)) to the current goal.

Let Z' and rZ be given.

We will prove Hom_struct_r (pack_r Y' rY) (pack_r Z' rZ) g → Hom_struct_r (pack_r X' rX) (pack_r Z' rZ) (lam_comp X' g f).

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

Assume Hg: g ∈ Z'^Y' ∧ (∀y y' ∈ Y', rY y y' → rZ (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', rX x x' → rZ (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' Hx2.

We will prove rZ ((λ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 rZ (g (f x)) (g (f x')).

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

Apply Hf2 x Hx x' Hx' to the current goal.

An exact proof term for the current goal is Hx2.