Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ο be given.
Apply unknownprop_334a5a4dfd5441f12538cd3c70458238b05308c372afbd4cf94b09dd8e7afe85 with
x0,
x1,
x2 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with
e4431.. x0,
e4431.. x1,
e4431.. x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply H3 with
x3 leaving 2 subgoals.
Apply unknownprop_ecae2d2d3708015d34ac3eacd84df17c3571bd5e56ae2362f9cb0de5042f4b16 with
x1,
x3 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
The subproof is completed by applying H15.
The subproof is completed by applying H11.
Apply unknownprop_ee5bcd8a678317db72ef3d355308c7e294e59766f08f82a0b083647c04eafd99 with
x0,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H14.
The subproof is completed by applying H10.
Apply H4.
Apply unknownprop_ecae2d2d3708015d34ac3eacd84df17c3571bd5e56ae2362f9cb0de5042f4b16 with
x1,
x0 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
Apply H5.
Apply unknownprop_ee5bcd8a678317db72ef3d355308c7e294e59766f08f82a0b083647c04eafd99 with
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
The subproof is completed by applying H2.