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