Let x0 of type ι be given.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
4a7ef..,
x0,
λ x1 x2 . prim1 x0 (4ae4a.. x1) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x0.