Let x0 of type ι be given.
Apply unknownprop_de75d6825d81b7a38884e6d5bfefe1b968fb72336b8dd0437226d27d493a019a with
x0,
0,
λ x1 x2 . x2 = 0.
The subproof is completed by applying unknownprop_524a01b901ce62fa6d32d4caeb3c7baa9e801388ce81f1633896f452e2f7d01c with x0.