Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_583d89fd1ad8d69ba9f546e19a854760a1fb18a1f5be71aa71ee27b6e6082be7 with
x1,
λ x2 x3 . equip (setprod x0 x3) 0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with
setprod x0 0,
λ x2 x3 . equip x3 0 leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
x2,
setprod x0 0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
proj1 x2.
Apply unknownprop_0ca88b304f8486344af25c1dccffdd0de0911b83400025c64b3ac2bfa45e498f with
x0,
0,
x2.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with 0.