Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
PER,
BinRelnHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_a9109a2e2c7b58d168a345c3d559fa6cefbb8aaf51b02c98b368d0383e86b3cc.
The subproof is completed by applying unknownprop_da50e7cfd4a6aa1a481b29d9a258b6246a088ccf7431433a7c842df63c835f1e.
The subproof is completed by applying unknownprop_7424d1576845fd7b3796312ad5767cec794f06149f4f042f760ca6e0fb95d565.