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