Apply unknownprop_546459d2e02981984519c87d69c9085ebffaa0d7c4326fca643e2a1b93719e6a with
λ x0 x1 : ι → ι . ∀ x2 . Subq x2 (x1 x2).
Let x0 of type ι be given.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x0,
(λ x1 . binunion x1 (Sing x1)) x0.
Let x1 of type ι be given.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with
x0,
Sing x0,
x1.
The subproof is completed by applying H0.