Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with
struct_r,
BinRelnHom,
struct_id,
struct_comp leaving 3 subgoals.
The subproof is completed by applying unknownprop_c743d500597c886f8c9f734201e1e33c3ed6306ca10b5ca232711b87a9244d05.
The subproof is completed by applying unknownprop_0bffcbc5d86f4ba074fd813ba32990cab76e7a4512be26e82f93761494dc7f3f.
The subproof is completed by applying unknownprop_907117947d3e5122f17dc0ad87d42ef61641eaa3908e950d289d200dd82717a4.