Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
EquivReln,
BinRelnHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_9b87477ddae5e1dddee7ca772cf97e36225e0c4d6c64a3a14907f878e8629023.
The subproof is completed by applying unknownprop_88bfe6d781381f29ef043aee3e2988fe3a72374427e3637d5ac3993ada29fd2a.
The subproof is completed by applying unknownprop_78f231cfd5c3d9e0f310265d5b946c5362d2175a87918560d372a043b147dbaa.