Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
IrreflexiveSymmetricReln,
BinRelnHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_53ea818e2021d87ac705f8683274896fc426e94dc27b29259138e0d21bd2ebcf.
The subproof is completed by applying unknownprop_df7a794afb6d0bc6aaf84f69a53154c30ebbe8d384f15e54a0f441d1cc9d4a7d.
The subproof is completed by applying unknownprop_3c8643c587af8b76606b3bd4c132b0669b42e58d4e2858afde92b9385ea31cd1.