Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_96da142705befb27f4d4cbde3ddc158cfc2a72a13b66b90c3f80ad788d6509a8 with
x0,
λ x4 . MagmaHom x4 x1 x2 ⟶ MagmaHom x4 x1 x3 ⟶ 6e587.. (32592.. x4 x1 x2 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Let x6 of type ι be given.
Assume H3: x6 ∈ x4.
Assume H4: ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x5 x7 x8 ∈ x4.
Assume H5:
∀ x7 . x7 ∈ x4 ⟶ and (x5 x7 x6 = x7) (x5 x6 x7 = x7).
Assume H6:
∀ x7 . x7 ∈ x4 ⟶ bij x4 x4 (x5 x7).
Assume H7:
∀ x7 . x7 ∈ x4 ⟶ bij x4 x4 (λ x8 . x5 x8 x7).
Apply unknownprop_96da142705befb27f4d4cbde3ddc158cfc2a72a13b66b90c3f80ad788d6509a8 with
x1,
λ x7 . MagmaHom (pack_b x4 x5) x7 x2 ⟶ MagmaHom (pack_b x4 x5) x7 x3 ⟶ 6e587.. (32592.. (pack_b x4 x5) x7 x2 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x7 of type ι be given.
Let x8 of type ι → ι → ι be given.
Let x9 of type ι be given.
Assume H8: x9 ∈ x7.
Assume H9: ∀ x10 . x10 ∈ x7 ⟶ ∀ x11 . x11 ∈ x7 ⟶ x8 x10 x11 ∈ x7.
Assume H10:
∀ x10 . x10 ∈ x7 ⟶ and (x8 x10 x9 = x10) (x8 x9 x10 = x10).
Assume H11:
∀ x10 . x10 ∈ x7 ⟶ bij x7 x7 (x8 x10).
Assume H12:
∀ x10 . x10 ∈ x7 ⟶ bij x7 x7 (λ x11 . x8 x11 x10).
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x4,
x7,
x5,
x8,
x2,
λ x10 x11 : ο . x11 ⟶ MagmaHom (pack_b x4 x5) (pack_b x7 x8) x3 ⟶ 6e587.. (32592.. (pack_b x4 x5) (pack_b x7 x8) x2 x3).
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x4,
x7,
x5,
x8,
x3,
λ x10 x11 : ο . and (x2 ∈ setexp x7 x4) (∀ x12 . x12 ∈ x4 ⟶ ∀ x13 . x13 ∈ x4 ⟶ ap x2 (x5 x12 x13) = x8 (ap x2 x12) (ap x2 x13)) ⟶ x11 ⟶ 6e587.. (32592.. (pack_b x4 x5) (pack_b x7 x8) x2 x3).
Assume H13:
and (x2 ∈ setexp x7 x4) (∀ x10 . ... ⟶ ∀ x11 . x11 ∈ ... ⟶ ap x2 (x5 x10 x11) = x8 (ap x2 x10) (ap x2 x11)).
Apply unknownprop_e61ba9aff4fd349c1c42f2a34d877d749901dbe2942e4d83737a99cb0fa8568b with
6e587.. leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.