Apply unknownprop_7286e98d609aa746e0fd442fb25d48ecc298d66ff863c06370951cf0a76dad5e with
λ x0 x1 : ι → ι . ∀ x2 . In x2 (x1 x2).
Let x0 of type ι be given.
The subproof is completed by applying unknownprop_f40d13744d00ec34b223eab4c005556ef718e0ee3d9e509403edfd952d571ca0 with x0, x0.