Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
6e587..,
MagmaHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_0638c3b4540642ea0f15fef73263da94e2cb00310bfc6a41a9602ac5c7f1d01e.
The subproof is completed by applying unknownprop_506ac0f9d1a76c21790b5dd767b1b8bbb959506568ba8a4211c93fda556a3d15.
The subproof is completed by applying unknownprop_8a471b469f51e7275518bd30bccb7b4cb19e74b974b028cdf79c1d4cbc665f9e.