Apply unknownprop_e61ba9aff4fd349c1c42f2a34d877d749901dbe2942e4d83737a99cb0fa8568b with
struct_b leaving 2 subgoals.
Let x0 of type ι be given.
The subproof is completed by applying H0.
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 H0 with
λ x4 . MagmaHom x4 x1 x2 ⟶ MagmaHom x4 x1 x3 ⟶ struct_b (32592.. x4 x1 x2 x3).
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Assume H2: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ∈ x4.
Apply H1 with
λ x6 . MagmaHom (pack_b x4 x5) x6 x2 ⟶ MagmaHom (pack_b x4 x5) x6 x3 ⟶ struct_b (32592.. (pack_b x4 x5) x6 x2 x3).
Let x6 of type ι be given.
Let x7 of type ι → ι → ι be given.
Assume H3: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ x7 x8 x9 ∈ x6.
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x4,
x6,
x5,
x7,
x2,
λ x8 x9 : ο . x9 ⟶ MagmaHom (pack_b x4 x5) (pack_b x6 x7) x3 ⟶ struct_b (32592.. (pack_b x4 x5) (pack_b x6 x7) x2 x3).
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
x4,
x6,
x5,
x7,
x3,
λ x8 x9 : ο . and (x2 ∈ setexp x6 x4) (∀ x10 . x10 ∈ x4 ⟶ ∀ x11 . x11 ∈ x4 ⟶ ap x2 (x5 x10 x11) = x7 (ap x2 x10) (ap x2 x11)) ⟶ x9 ⟶ struct_b (32592.. (pack_b x4 x5) (pack_b x6 x7) x2 x3).
Assume H4:
and (x2 ∈ setexp x6 x4) (∀ x8 . x8 ∈ x4 ⟶ ∀ x9 . x9 ∈ x4 ⟶ ap x2 (x5 x8 x9) = x7 (ap x2 x8) (ap x2 x9)).
Assume H5:
and (x3 ∈ setexp x6 x4) (∀ x8 . x8 ∈ x4 ⟶ ∀ x9 . x9 ∈ x4 ⟶ ap x3 (x5 x8 x9) = x7 (ap x3 x8) (ap x3 x9)).