Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
9f253..,
UnaryFuncHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_2568db697e5888ec2fd1f1bf9456b9508292ed4b824e8582b40e4f025f149e68.
The subproof is completed by applying unknownprop_b2b78fdc216cab07060e9c76e5fe1a36b1c7bdd4ef12656122c37f5290a80907.
The subproof is completed by applying unknownprop_4dd455371a48ff8f053838210afdce9a3002e9898445c300e57535dc175841cb.