Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
Let x13 of type ι be given.
Let x14 of type ι be given.
Let x15 of type ι be given.
Let x16 of type ι be given.
Apply unknownprop_47518985ef28bbb9c43dba4f29b3a0586668c84ce7b1b9270ee3db2f856a5f78 with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12,
x13,
x14,
x15,
x16 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d3916f6a6fcb01be833f85d8ad2b81dc017a5825678ddb80185d00cb4ac630dc.
The subproof is completed by applying unknownprop_63c13366871d56b929a86e30fe3f917efdeb3d770effb105bd4d58ad234e36b2.