Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply unknownprop_4d43d3c800597522c7877c12c57585d0d8c2187c991fb24d3cbd7ddd8a9e982b with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_0d44ecefd0d38f8f5126e10a2df200121ed6d55bbd9cc78a15a6bd161c22011e with
x0,
PSNo x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L1.
Apply unknownprop_97c7da29e9595b010ed33a7cba4535d53c32ea3bcafdf9fb46c420ab4230017e with
PSNo x0 x1,
SNoLev (PSNo x0 x1) = x0 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply unknownprop_7a09c591c3f493c02f06dbfea360001bad64009e8d65cd32a32f96aed3daa8a0 with
PSNo x0 x1,
SNoLev (PSNo x0 x1),
x0 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying L1.