definition invert_bs_relation ≝
λC:bishop_set.λU:C squareB → Prop.
λx:C squareB. U 〈\snd x,\fst x〉.
notation > "\inv" with precedence 60 for @{ 'invert_symbol }.
definition invert_bs_relation ≝
λC:bishop_set.λU:C squareB → Prop.
λx:C squareB. U 〈\snd x,\fst x〉.
notation > "\inv" with precedence 60 for @{ 'invert_symbol }.