Apply unknownprop_4952cbeaa3cfbe39042137e565a281ffc28405c7de4fe454358dcf1400b68a14 with
1,
λ x0 x1 . 0.
Let x0 of type ι be given.
Let x1 of type ι be given.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.