Proving Congruence of Bisimulation in Functional Programming Languages