moved a.paste to RelationProperties, inlined notation; renamed b.ll09 → RelationProperties.paste_subrel, optimised proof