for C1, C2 being 1-sorted
for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds
M is coreflexive