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).