Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
SelfInjection,
UnaryFuncHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_a7df09be51260a7802a2d4dba43c36f3ce14e7adc5b5c9b8b2580df2aa5ad63b.
The subproof is completed by applying unknownprop_c671edd1a4531bd90b313e69dbf29f5cf070f1aba7fc6b5ba46ca33174251409.
The subproof is completed by applying unknownprop_d16054b5a46b72b66b2bb9dbc7cd666d2a1a3d3a0c3b10898d3b0033474cde18.