Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_1df4bfe22f97512506ab6eba7670da5964bce053975b48ab4bfcd7dc5cc40416 with
f4b0e.. x0 x1 x2 x3,
7cd66.. (f4b0e.. x0 x1 x2 x3) = x3 leaving 2 subgoals.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with
x0,
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x4 of type ι → ι → ο be given.
Apply unknownprop_103a081e403793937d3065fae3fde1756efbefb7dcc44a50b4b18345b916d030 with
x0,
x1,
x2,
x3,
6b27d.. (f4b0e.. x0 x1 x2 x3),
e5fe3.. (f4b0e.. x0 x1 x2 x3),
e47cc.. (f4b0e.. x0 x1 x2 x3),
7cd66.. (f4b0e.. x0 x1 x2 x3),
λ x5 x6 . x4 x6 x5 leaving 9 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_d490e9b67b13d1ef9389d3ace4e99a44b8ce86dd1d81aca7dab87729606ec525 with
f4b0e.. x0 x1 x2 x3.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with
x0,
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_221fdb669888182bab57f3018210dac7aa6f39893e1d9c3490c39bcf8bddffeb with
f4b0e.. x0 x1 x2 x3.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with
x0,
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_8c3e941e183588bb9845a8e92af7c2409f09ad8e12d04378912de4f735a7c469 with
f4b0e.. x0 x1 x2 x3.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with
x0,
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_072d8bdde21ee9f95ca6908fd1694154122013121af055783afb363ccc47d946 with
f4b0e.. x0 x1 x2 x3.
Apply unknownprop_1c4b77a1bdf71ac8c46772d8b01bd6609e54ee74070e16498c4800adfe13c5ca with
x0,
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.