Assume HO.
Apply MetaCatConcrete Obj (λX ⇒ X 0) Hom_struct_u to the current goal.
Let X, Y and f be given.
Assume HX HY.
Apply HO X HX (λu ⇒ Hom_struct_u u Y f → f ∈ Y 0u 0) to the current goal.
Let X' and uX be given.
Assume HuX.
Apply HO Y HY (λu ⇒ Hom_struct_u (pack_u X' uX) u f → f ∈ u 0pack_u X' uX 0) to the current goal.
Let Y' and uY be given.
Assume HuY.
We will prove Hom_struct_u (pack_u X' uX) (pack_u Y' uY) f → f ∈ pack_u Y' uY 0pack_u X' uX 0.
rewrite the current goal using Hom_struct_u_pack (from left to right).
Assume Hf: f ∈ Y'X' ∧ (∀x ∈ X', f (uX x) = uY (f x)).
Apply Hf to the current goal.
Assume Hf1 Hf2.
rewrite the current goal using pack_u_0_eq2 (from right to left).
rewrite the current goal using pack_u_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_u u u (lam_id (u 0))) to the current goal.
Let X' and uX be given.
Assume HuX.
We will prove Hom_struct_u (pack_u X' uX) (pack_u X' uX) (lam_id (pack_u X' uX 0)).
rewrite the current goal using pack_u_0_eq2 (from right to left).
rewrite the current goal using Hom_struct_u_pack (from left to right).
We will prove lam_id X' ∈ X'X' ∧ (∀x ∈ X', lam_id X' (uX x) = uX (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.
We will prove lam_id X' (uX x) = uX ((λ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 beta X' (λx ⇒ x) (uX x) (HuX x Hx).
Let X, Y, Z, f and g be given.
Assume HX HY HZ.
Apply HO X HX (λu ⇒ Hom_struct_u u Y f → Hom_struct_u Y Z g → Hom_struct_u u Z (lam_comp (u 0) g f)) to the current goal.
Let X' and uX be given.
Assume HuX.
We will prove Hom_struct_u (pack_u X' uX) Y f → Hom_struct_u Y Z g → Hom_struct_u (pack_u X' uX) Z (lam_comp (pack_u X' uX 0) g f).
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove Hom_struct_u (pack_u X' uX) Y f → Hom_struct_u Y Z g → Hom_struct_u (pack_u X' uX) Z (lam_comp X' g f).
Apply HO Y HY (λu ⇒ Hom_struct_u (pack_u X' uX) u f → Hom_struct_u u Z g → Hom_struct_u (pack_u X' uX) Z (lam_comp X' g f)) to the current goal.
Let Y' and uY be given.
Assume HuY.
We will prove Hom_struct_u (pack_u X' uX) (pack_u Y' uY) f → Hom_struct_u (pack_u Y' uY) Z g → Hom_struct_u (pack_u X' uX) Z (lam_comp X' g f).
rewrite the current goal using Hom_struct_u_pack (from left to right).
Assume Hf: f ∈ Y'X' ∧ (∀x ∈ X', f (uX x) = uY (f x)).
Apply HO Z HZ (λu ⇒ Hom_struct_u (pack_u Y' uY) u g → Hom_struct_u (pack_u X' uX) u (lam_comp X' g f)) to the current goal.
Let Z' and uZ be given.
Assume HuZ.
We will prove Hom_struct_u (pack_u Y' uY) (pack_u Z' uZ) g → Hom_struct_u (pack_u X' uX) (pack_u Z' uZ) (lam_comp X' g f).
rewrite the current goal using Hom_struct_u_pack (from left to right).
rewrite the current goal using Hom_struct_u_pack (from left to right).
Assume Hg: g ∈ Z'Y' ∧ (∀y ∈ Y', g (uY y) = uZ (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', lam_comp X' g f (uX x) = uZ (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.
We will prove lam_comp X' g f (uX x) = uZ ((λ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 (λx ∈ X' ⇒ g (f x)) (uX x) = uZ (g (f x)).
rewrite the current goal using beta X' (λx ⇒ g (f x)) (uX x) (HuX x Hx) (from left to right).
We will prove g (f (uX x)) = uZ (g (f x)).
rewrite the current goal using Hg2 (f x) (ap_Pi X' (λ_ ⇒ Y') f x Hf1 Hx) (from right to left).
We will prove g (f (uX x)) = g (uY (f x)).
Use f_equal.
An exact proof term for the current goal is Hf2 x Hx.
∎