Let x0 of type ι be given.
Apply unknownprop_70ac04d26d82d55a8a7aa1e3e5b0320484a1911a0615cda02457d07c571bd97b with
x0,
λ x1 x2 . In 0 x2.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with
Sing 0,
Repl x0 (λ x1 . Inj1 x1),
0.
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 0.