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