Let x0 of type ι be given.
Apply unknownprop_05c5f12266552972e2f6bb79dd7296b83fbb97fdcc61f58126e0634ad7058280 with
x0,
λ x1 x2 . ∀ x3 . equip x3 x0 ⟶ equip (setexp x3 2) x2.
Apply unknownprop_a8fb94cb228e26cf51c99a0f2700abe23ab117f4f88f1f75bbc15333b4951e10 with
x0.
The subproof is completed by applying H0.