  Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and
Jacobs suggest to focus on apartness, which they define by dualising
coalgebraic bisimulations. This yields the possibility of finite proofs of
distinguishability for a wide variety of state-based systems.
  We propose behavioural apartness, defined by dualising behavioural
equivalence rather than bisimulations. A motivating example is the
subdistribution functor, where the proof system based on bisimilarity requires
an infinite quantification over couplings, whereas behavioural apartness
instantiates to a finite rule. In addition, we provide optimised proof rules
for behavioural apartness and show their use in several examples.
