Let x0 of type ι be given.
Apply unknownprop_c3bea5de1408165b06631f86b9f132e6a4154b60456b567e9159f0db1e9656af with
x0,
4a7ef..,
λ x1 x2 . x2 = 4a7ef...
The subproof is completed by applying unknownprop_b0ef46c91c1741efb5e7596e49359a2bfaa6712fd07df6250122f389bd89e619 with x0.