Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
Group,
MagmaHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_7f680c301fd042c0aae25972d0e8efbaf05b2c058517555e5d05a60e38df7062.
The subproof is completed by applying unknownprop_c5cb8c189435e8d454517c35606123a25b977570e8025d6d05eabab91ff33a60.
The subproof is completed by applying unknownprop_5c6bb5f9257e42e0c3a0f92afe0403afb3ceec6a5da6e162940022fa7b541077.