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_2f1d491922dcc2c2c85957b7d88dc1d40484f0719168a164b34095ed29478f03 with
x0,
λ x4 . UnaryFuncHom x4 x1 x2 ⟶ UnaryFuncHom x4 x1 x3 ⟶ SelfInjection (9fd7a.. 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.
Assume H3: ∀ x6 . x6 ∈ x4 ⟶ x5 x6 ∈ x4.
Assume H4: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 = x5 x7 ⟶ x6 = x7.
Apply unknownprop_2f1d491922dcc2c2c85957b7d88dc1d40484f0719168a164b34095ed29478f03 with
x1,
λ x6 . UnaryFuncHom (pack_u x4 x5) x6 x2 ⟶ UnaryFuncHom (pack_u x4 x5) x6 x3 ⟶ SelfInjection (9fd7a.. (pack_u x4 x5) x6 x2 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x6 of type ι be given.
Let x7 of type ι → ι be given.
Assume H5: ∀ x8 . x8 ∈ x6 ⟶ x7 x8 ∈ x6.
Assume H6: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ x7 x8 = x7 x9 ⟶ x8 = x9.
Apply unknownprop_c0506b7ce99ca057359584255bdeac2239c78bf84c4390e2fc4c72ca99c22cfa with
x4,
x6,
x5,
x7,
x2,
λ x8 x9 : ο . x9 ⟶ UnaryFuncHom (pack_u x4 x5) (pack_u x6 x7) x3 ⟶ SelfInjection (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 ⟶ SelfInjection (9fd7a.. (pack_u x4 x5) (pack_u x6 x7) x2 x3).
Assume H7:
and (x2 ∈ setexp x6 x4) (∀ x8 . x8 ∈ x4 ⟶ ap x2 (x5 x8) = x7 (ap x2 x8)).
Apply unknownprop_dcc815a24b87cf3130afd70cd64a2143fe42bc8fb9cd4174cad915c8a51f1e00 with
SelfInjection leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.