interpretation "relation invertion" 'invert a = (invert_bs_relation ? a).
interpretation "relation invertion" 'invert_symbol = (invert_bs_relation ?).
interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation ? a x).
interpretation "relation invertion" 'invert a = (invert_bs_relation ? a).
interpretation "relation invertion" 'invert_symbol = (invert_bs_relation ?).
interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation ? a x).