Make EquationTree proof producing, introduce Congruence inference types