Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_901227726ecb21c0c865a7b1769191cd65e10f479fbeb543b259399303379e3e with
x0,
x1,
4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_e5c1596f5fd6bc2d713145a4e9d44688423a48751f219f9d9d142effb814941e.
Apply unknownprop_d703849eb8e5f2d3b12754a845ec7b0f82607397d42827babfa4298acd2176ee with
x0,
λ x2 x3 . prim1 x1 x3.
The subproof is completed by applying H0.