Let x0 of type ι be given.
Apply unknownprop_6e6ce909b9c17abe947e3e080426f45a329a4c2db70cb2c91959a2db175cdfa8 with
x0,
prim0 (aa8d2.. 4a7ef.. x0).
Apply unknownprop_90bcc02ecc46b92df3edbe0008c0f8bb530ab6a017204b007fade1bade9af775 with
4a7ef..,
x0.
The subproof is completed by applying unknownprop_e5c1596f5fd6bc2d713145a4e9d44688423a48751f219f9d9d142effb814941e.