Let x0 of type ι be given.
Apply unknownprop_3189570886a432a72e87efcbd0ea995fafcd88c6ec3c7fdffceb2e344a826cdc with
x0,
λ x1 x2 . Subq (setsum x1 (ap x0 1)) x0.
Apply unknownprop_3030666c70e3b0a40e79c3dea18074452b4f067cae53efb13b5a85e3938a9613 with
x0,
λ x1 x2 . Subq (setsum (proj0 x0) x1) x0.
The subproof is completed by applying unknownprop_a059c9c6c5f191867e77960aa3f6a8924a5c904b8b3d051226c2dcca8aa8daee with x0.