Let x0 of type ι be given.
Apply unknownprop_73b312e5c0ced1987581817c61d2a6ab9e4c47a87f99557a6b2723117244e7d9 with
binintersect 0 x0.
The subproof is completed by applying unknownprop_e0d452e0e0459ccd22d0a0ca66d8c6b520f69a835c0ebd50bbdd40077efd4a68 with 0, x0.