On coinductive equivalences for higher-order probabilistic functional programs