Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
Quasigroup,
MagmaHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_9c0f3e1afa76ce315f77d47a5f99937a75bb29d19734ab916f215622174a2062.
The subproof is completed by applying unknownprop_422d84a9aa4eecb2ea178ab0e1d12e0b1a76b35e8bbf6ae00962c4b27ac61fcf.
The subproof is completed by applying unknownprop_f456a6b28a403228d3cc02efff12ad99c90b24514643982c96a491b18d323ebe.