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