Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
struct_b,
MagmaHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_cb8d374538fe4eed29e0b446edf32f6afed5fe007be224a383b378d00bb23030.
The subproof is completed by applying unknownprop_9ae50e20818be24e83feab8446d73e9df96ee358b7d80e64a0e2f213eb2bafb4.
The subproof is completed by applying unknownprop_d64c39226526628145b86e9223e08aecec3869793d2381afbab7431e95412a95.