Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_bf35ed077052d180738002d3131b9c960f2105b6fc771a9376424dc88c5accaa with
x0.
The subproof is completed by applying H0.
Apply unknownprop_f4589932e78557c04376dc773ac7e96363fb72f89bfabb77016339bd41fdf147 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_bf35ed077052d180738002d3131b9c960f2105b6fc771a9376424dc88c5accaa with
x1.
The subproof is completed by applying H1.
Apply unknownprop_f4589932e78557c04376dc773ac7e96363fb72f89bfabb77016339bd41fdf147 with
x1.
The subproof is completed by applying H1.