Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Assume H2: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x0,
x2,
x1,
x3,
x4,
λ x6 x7 : ο . x7 ⟶ MagmaHom (pack_b x0 x1) (pack_b x2 x3) x5 ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ {x10 ∈ x0|ap x4 x10 = ap x5 x10} ⟶ ∀ x10 . x10 ∈ {x11 ∈ x0|ap x4 x11 = ap x5 x11} ⟶ x1 x9 x10 = x8 x9 x10) ⟶ 28b0a.. {x9 ∈ x0|ap x4 x9 = ap x5 x9} x8.
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x0,
x2,
x1,
x3,
x5,
λ x6 x7 : ο . and (x4 ∈ setexp x2 x0) (∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ap x4 (x1 x8 x9) = x3 (ap x4 x8) (ap x4 x9)) ⟶ x7 ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . x9 ∈ {x10 ∈ x0|ap x4 x10 = ap x5 x10} ⟶ ∀ x10 . x10 ∈ {x11 ∈ x0|ap x4 x11 = ap x5 x11} ⟶ x1 x9 x10 = x8 x9 x10) ⟶ 28b0a.. {x9 ∈ x0|ap x4 x9 = ap x5 x9} x8.
Assume H4:
and (x4 ∈ setexp x2 x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ap x4 (x1 x6 x7) = x3 (ap x4 x6) (ap x4 x7)).
Apply H4 with
and (x5 ∈ setexp x2 x0) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ap x5 (x1 x6 x7) = x3 (ap x5 x6) (ap x5 x7)) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . x7 ∈ {x8 ∈ x0|ap x4 x8 = ap x5 x8} ⟶ ∀ x8 . x8 ∈ {x9 ∈ x0|ap x4 x9 = ap x5 x9} ⟶ x1 x7 x8 = x6 x7 x8) ⟶ 28b0a.. {x7 ∈ x0|ap x4 x7 = ap x5 x7} x6.
Assume H6:
∀ x6 . ... ⟶ ∀ x7 . ... ⟶ ap ... ... = ....