Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
struct_p,
UnaryPredHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_edb0bbc1cf315b54e2af6e88f0ad67b20f207887129fd2bc159319d8845a3b71.
The subproof is completed by applying unknownprop_43a3b1d383dbc17cf0fad4f17bdb8738ca59e8c49eac4667ce75cc8fa7a35240.
The subproof is completed by applying unknownprop_097713311b3a8f262dee5be9217eb9add9c303ef2514caa7f22ffa90c0bd6955.