Apply unknownprop_8e67f22739f9a01fd2d9438edd2f3f6d8d323d1fa4d050bc09f5b1af8d3b6dd7 with
λ x0 x1 . equip (prim4 u5) x0.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
u5.
The subproof is completed by applying nat_5.