Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
Semigroup,
MagmaHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_246240c73ebc2d1b98473699e9f191b933ab66db45ae7b22cab2d486ffc81da1.
The subproof is completed by applying unknownprop_b8cc50a234b019d0503b700b1125ddeecceb1ee1041bce87e347d228251529b8.
The subproof is completed by applying unknownprop_d5b8a1af9413ec92ffb1b879b94b07b76a4ffae06221146bc06149f479010c1d.