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_3d05796578cdc17ebd2096167db48ecef934256d250d1637eb5dd67225cdfe05 with
x0,
x1,
x2,
x3,
x0,
x1,
x2,
x3,
λ x4 . x4,
λ x4 x5 x6 . x6 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_ee743b29f4e621eaebf8076162c85fcf9e1b886cf72f6c3b7435ceaddea4388a with x0, x1, x2, x3.