Apply H1 with
False.
Let x0 of type ι be given.
Apply H2 with
False.
Let x1 of type ι → ι be given.
Apply H3 with
False.
Apply H4 with
(∀ x2 . Monoid x2 ⟶ and (MagmaHom x0 x2 (x1 x2)) (∀ x3 . MagmaHom x0 x2 x3 ⟶ x3 = x1 x2)) ⟶ False.
Apply H5 with
λ x2 . unpack_b_o x2 (λ x3 . λ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ ∀ x7 . x7 ∈ x3 ⟶ x4 (x4 x5 x6) x7 = x4 x5 (x4 x6 x7)) (∃ x5 . and (x5 ∈ x3) (∀ x6 . x6 ∈ x3 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6)))) ⟶ (∀ x3 . Monoid x3 ⟶ and (MagmaHom x2 x3 (x1 x3)) (∀ x4 . MagmaHom x2 x3 x4 ⟶ x4 = x1 x3)) ⟶ False.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Assume H6: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2.
Apply unpack_b_o_eq with
λ x4 . λ x5 : ι → ι → ι . and (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x5 (x5 x6 x7) x8 = x5 x6 (x5 x7 x8)) (∃ x6 . and (x6 ∈ x4) (∀ x7 . x7 ∈ x4 ⟶ and (x5 x7 x6 = x7) (x5 x6 x7 = x7))),
x2,
x3,
λ x4 x5 : ο . x5 ⟶ (∀ x6 . Monoid x6 ⟶ and (MagmaHom (pack_b x2 x3) x6 (x1 x6)) (∀ x7 . MagmaHom (pack_b x2 x3) x6 x7 ⟶ x7 = x1 x6)) ⟶ False leaving 2 subgoals.
Apply L0 with
x2,
x3.
The subproof is completed by applying H6.
Assume H7:
(λ x4 . λ x5 : ι → ι → ι . and (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x5 (x5 x6 x7) x8 = x5 x6 (x5 x7 x8)) (∃ x6 . and (x6 ∈ x4) (∀ x7 . x7 ∈ x4 ⟶ and (x5 x7 x6 = x7) (x5 x6 x7 = x7)))) x2 x3.