Apply unknownprop_dcc815a24b87cf3130afd70cd64a2143fe42bc8fb9cd4174cad915c8a51f1e00 with
struct_u 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 . UnaryFuncHom x4 x1 x2 ⟶ UnaryFuncHom x4 x1 x3 ⟶ struct_u (9fd7a.. x4 x1 x2 x3).
Let x4 of type ι be given.
Let x5 of type ι → ι be given.
Assume H2: ∀ x6 . x6 ∈ x4 ⟶ x5 x6 ∈ x4.
Apply H1 with
λ x6 . UnaryFuncHom (pack_u x4 x5) x6 x2 ⟶ UnaryFuncHom (pack_u x4 x5) x6 x3 ⟶ struct_u (9fd7a.. (pack_u x4 x5) x6 x2 x3).
Let x6 of type ι be given.
Let x7 of type ι → ι be given.
Assume H3: ∀ x8 . x8 ∈ x6 ⟶ x7 x8 ∈ x6.
Apply unknownprop_c0506b7ce99ca057359584255bdeac2239c78bf84c4390e2fc4c72ca99c22cfa with
x4,
x6,
x5,
x7,
x2,
λ x8 x9 : ο . x9 ⟶ UnaryFuncHom (pack_u x4 x5) (pack_u x6 x7) x3 ⟶ struct_u (9fd7a.. (pack_u x4 x5) (pack_u x6 x7) x2 x3).
Apply unknownprop_c0506b7ce99ca057359584255bdeac2239c78bf84c4390e2fc4c72ca99c22cfa with
x4,
x6,
x5,
x7,
x3,
λ x8 x9 : ο . and (x2 ∈ setexp x6 x4) (∀ x10 . x10 ∈ x4 ⟶ ap x2 (x5 x10) = x7 (ap x2 x10)) ⟶ x9 ⟶ struct_u (9fd7a.. (pack_u x4 x5) (pack_u x6 x7) x2 x3).
Assume H4:
and (x2 ∈ setexp x6 x4) (∀ x8 . x8 ∈ x4 ⟶ ap x2 (x5 x8) = x7 (ap x2 x8)).
Assume H5:
and (x3 ∈ setexp x6 x4) (∀ x8 . x8 ∈ x4 ⟶ ap x3 (x5 x8) = x7 (ap x3 x8)).
Apply H4 with
struct_u (9fd7a.. (pack_u x4 x5) (pack_u x6 x7) x2 x3).
Assume H7:
∀ x8 . x8 ∈ x4 ⟶ ap x2 (x5 x8) = x7 (ap x2 x8).
Apply H5 with
struct_u (9fd7a.. (pack_u x4 x5) (pack_u x6 x7) x2 x3).
Assume H9:
∀ x8 . x8 ∈ x4 ⟶ ap x3 (x5 x8) = x7 (ap x3 x8).
Apply unknownprop_f4bb4a323312a4b632fa1e16b0c97b44cc82e8e332928b09af21c3ea10e45603 with
x4,
x5,
pack_u x6 x7,
x2,
x3,
λ x8 x9 . struct_u x9.
Apply pack_struct_u_I with
{x8 ∈ x4|ap x2 x8 = ap x3 x8},
x5.
Let x8 of type ι be given.
Assume H10:
x8 ∈ {x9 ∈ x4|ap x2 x9 = ap x3 x9}.
Apply SepE with
x4,
λ x9 . ap x2 x9 = ap x3 x9,
x8,
x5 x8 ∈ {x9 ∈ x4|...} leaving 2 subgoals.