Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ι be given.
Let x4 of type ι → ι be given.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x0,
x1,
x3,
inj x0 x2 (λ x5 . x4 (x3 x5)) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2:
∀ x5 . In x5 x0 ⟶ In (x3 x5) x1.
Assume H3:
∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ x3 x5 = x3 x6 ⟶ x5 = x6.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x1,
x2,
x4,
inj x0 x2 (λ x5 . x4 (x3 x5)) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H4:
∀ x5 . In x5 x1 ⟶ In (x4 x5) x2.
Assume H5:
∀ x5 . In x5 x1 ⟶ ∀ x6 . In x6 x1 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
x0,
x2,
λ x5 . x4 (x3 x5) leaving 2 subgoals.
Let x5 of type ι be given.
Apply H4 with
x3 x5.
Apply H2 with
x5.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H8: x4 (x3 x5) = x4 (x3 x6).
Apply H3 with
x5,
x6 leaving 3 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Apply H5 with
x3 x5,
x3 x6 leaving 3 subgoals.
Apply H2 with
x5.
The subproof is completed by applying H6.
Apply H2 with
x6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.