Apply unknownprop_cd2abc9a9ea77fa61ee84765e1ca3a91f36a1f29e455a4bb2f3f1707f68cbca0 with
λ x0 x1 . equip (setprod u6 u6) x0.
Apply equip_sym with
mul_nat u6 u6,
setprod u6 u6.
Apply unknownprop_b67c3f99b7dcb350283e28e0205622aac5c4480ca587d55b1fc9b439a7a164e1 with
u6,
u6,
u6,
u6 leaving 4 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying nat_6.
The subproof is completed by applying equip_ref with
u6.
The subproof is completed by applying equip_ref with
u6.