Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
struct_u,
UnaryFuncHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_5de12671ce5578185e763d350f97672aefc724365fc2efb408ee27de0205dcd6.
The subproof is completed by applying unknownprop_a411183f2714db4c55dafde25e801653ef22805f13b242b9705e625f2ca37e08.
The subproof is completed by applying unknownprop_1c55d41ada92373a7dae22f8f024ba181c871faff35067ddb3e492aa9a1c43d7.