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