Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_5843a53f522dbf92d80ac36289685067f008fd2f46b9067d54fc3bf68053a1a3 with
x1,
f482f.. x0 4a7ef..,
f482f.. x0 (4ae4a.. 4a7ef..).
Apply H0 with
λ x2 x3 . prim1 x3 x1.
The subproof is completed by applying H1.