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_355c2eec330de3847f8acb94d0fa17afee88aa6d8e0b995d329bf209f1ac5c7a with
x0,
x1,
x2,
x3 leaving 6 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 H4.
Apply unknownprop_3bb88212dd853920577537bc3ecbc5e3e2bf8309e1e59246b79ae30400fc333e with
x1,
x3.
The subproof is completed by applying H5.