Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
Permutation,
UnaryFuncHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_97a117a3ef894b9fb1eb62c8aa64ff80223ce0478dc6c7c7a52d9ae80a2a2a33.
The subproof is completed by applying unknownprop_1c2881379aebcf1eee45af594b5e1f7fde32238b1cf231bfc78f0c2f9b3e76f5.
The subproof is completed by applying unknownprop_6b82cc4f1f3544ac2df4b4ad415f1160315dbeba5abc63ae2f7ac2467f252294.