Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_9cbe1b438cb309fdaf3dcacebb3b572a10a17828098a582be8e9441d5a1eab25 with
λ x2 x3 : ι → ι → ι . ∀ x4 . In x4 (x3 x1 x0) ⟶ ∀ x5 . In x5 (x3 x1 x0) ⟶ (∀ x6 . In x6 x0 ⟶ ap x4 x6 = ap x5 x6) ⟶ x4 = x5.
The subproof is completed by applying unknownprop_ce7d670de2cdb6f4a0f4372c09704540622a9299e7fe8f1e271df6d78a27a899 with x0, λ x2 . x1.