Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_80b6b34015b946fb84dd6201eac940043011b093e352907090feaca14c9fa11e with
4ec03.. x0 x1.
The subproof is completed by applying unknownprop_e16bc2988d24912b802d992f5a8cb11ec99a63284d8c426dcd0d04382e752862 with x0, x1.