Set Obj to be the term struct_b_monoid.
Set Hom to be the term Hom_struct_b.
Set id to be the term struct_id.
Set comp to be the term struct_comp.
Set Phi to be the term λX' op ⇒ (∀x y z ∈ X', op (op x y) z = op x (op y z)) ∧ (∃e ∈ X', ∀x ∈ X', op x e = x ∧ op e x = x) of type set → (set → set → set) → prop.
We prove the intermediate claim LPhi1: ∀X, ∀F : set → set → set, (∀x y ∈ X, F x y ∈ X) → ∀F' : set → set → set, (∀x y ∈ X, F x y = F' x y) → Phi X F' = Phi X F.
An exact proof term for the current goal is struct_b_monoid_Phi.
Assume H.
Apply H to the current goal.
Let Y be given.
Assume H.
Apply H to the current goal.
Let uniqa be given.
Assume H1: initial_p struct_b_monoid Hom_struct_b struct_id struct_comp Y uniqa.
Apply H1 to the current goal.
Assume HY: Obj Y.
Apply HY to the current goal.
Assume HYs.
Apply HYs to the current goal.
Let V and q be given.
Assume Hq.
rewrite the current goal using unpack_b_o_eq Phi V q (LPhi1 V q Hq) (from left to right).
Assume HVq: Phi V q.
Assume H2: ∀X : set, Obj X → Hom (pack_b V q) X (uniqa X) ∧ ∀h' : set, Hom (pack_b V q) X h' → h' = uniqa X.
Set M2 to be the term pack_b 2 mul_SNo.
We prove the intermediate claim L2SNo: ∀x ∈ 2, SNo x.
Let x be given.
Assume Hx.
An exact proof term for the current goal is omega_SNo x (nat_p_omega x (nat_p_trans 2 nat_2 x Hx)).
We prove the intermediate claim L1: Obj M2.
We will prove struct_b M2 ∧ unpack_b_o M2 Phi.
We prove the intermediate claim L1a: ∀x y ∈ 2, x * y ∈ 2.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
We prove the intermediate claim Ly: SNo y.
An exact proof term for the current goal is L2SNo y Hy.
Apply cases_2 x Hx to the current goal.
We will prove 0 * y ∈ 2.
rewrite the current goal using mul_SNo_zeroL y Ly (from left to right).
An exact proof term for the current goal is In_0_2.
We will prove 1 * y ∈ 2.
rewrite the current goal using mul_SNo_oneL y Ly (from left to right).
An exact proof term for the current goal is Hy.
Apply andI to the current goal.
Apply pack_struct_b_I to the current goal.
An exact proof term for the current goal is L1a.
rewrite the current goal using unpack_b_o_eq Phi 2 mul_SNo (LPhi1 2 mul_SNo L1a) (from left to right).
Apply andI to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Let z be given.
Assume Hz.
We will prove (x * y) * z = x * (y * z).
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc x y z (L2SNo x Hx) (L2SNo y Hy) (L2SNo z Hz).
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is In_1_2.
Let x be given.
Assume Hx.
We prove the intermediate claim Lx: SNo x.
An exact proof term for the current goal is L2SNo x Hx.
Apply andI to the current goal.
We will prove x * 1 = x.
An exact proof term for the current goal is mul_SNo_oneR x Lx.
We will prove 1 * x = x.
An exact proof term for the current goal is mul_SNo_oneL x Lx.
Apply H2 M2 L1 to the current goal.
rewrite the current goal using Hom_struct_b_pack (from left to right).
Assume H.
Apply H to the current goal.
Assume H3: uniqa M2 ∈ 2V.
Assume H4: ∀x y ∈ V, uniqa M2 (q x y) = uniqa M2 x * uniqa M2 y.
Assume H4: ∀h' : set, Hom (pack_b V q) M2 h' → h' = uniqa M2.
Set f to be the term λx ∈ V ⇒ 0.
Set g to be the term λx ∈ V ⇒ 1.
We prove the intermediate claim L2: Hom (pack_b V q) M2 f.
rewrite the current goal using Hom_struct_b_pack (from left to right).
Apply andI to the current goal.
We will prove f ∈ 2V.
We will prove (λx ∈ V ⇒ 0) ∈ ∏x ∈ V, 2.
Apply lam_Pi to the current goal.
Let x be given.
Assume Hx.
An exact proof term for the current goal is In_0_2.
We will prove ∀x y ∈ V, f (q x y) = f x * f y.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using beta V (λ_ ⇒ 0) (q x y) (Hq x Hx y Hy) (from left to right).
rewrite the current goal using beta V (λ_ ⇒ 0) x Hx (from left to right).
rewrite the current goal using beta V (λ_ ⇒ 0) y Hy (from left to right).
We will prove 0 = 0 * 0.
Use symmetry.
An exact proof term for the current goal is mul_SNo_zeroL 0 SNo_0.
We prove the intermediate claim L3: Hom (pack_b V q) M2 g.
rewrite the current goal using Hom_struct_b_pack (from left to right).
Apply andI to the current goal.
We will prove g ∈ 2V.
We will prove (λx ∈ V ⇒ 1) ∈ ∏x ∈ V, 2.
Apply lam_Pi to the current goal.
Let x be given.
Assume Hx.
An exact proof term for the current goal is In_1_2.
We will prove ∀x y ∈ V, g (q x y) = g x * g y.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
rewrite the current goal using beta V (λ_ ⇒ 1) (q x y) (Hq x Hx y Hy) (from left to right).
rewrite the current goal using beta V (λ_ ⇒ 1) x Hx (from left to right).
rewrite the current goal using beta V (λ_ ⇒ 1) y Hy (from left to right).
We will prove 1 = 1 * 1.
Use symmetry.
An exact proof term for the current goal is mul_SNo_oneL 1 SNo_1.
We will prove False.
Apply HVq to the current goal.
Assume HA: ∀x y z ∈ V, q (q x y) z = q x (q y z).
Assume H.
Apply H to the current goal.
Let e be given.
Assume H.
Apply H to the current goal.
Assume He: e ∈ V.
Assume _.
Apply neq_0_1 to the current goal.
We will prove 0 = 1.
Use transitivity with f e, uniqa M2 e, and g e.
We will prove 0 = f e.
Use symmetry.
An exact proof term for the current goal is beta V (λ_ ⇒ 0) e He.
We will prove f e = uniqa M2 e.
Use f_equal.
An exact proof term for the current goal is H4 f L2.
We will prove uniqa M2 e = g e.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is H4 g L3.
We will prove g e = 1.
An exact proof term for the current goal is beta V (λ_ ⇒ 1) e He.
∎