[STATEMENT]
lemma cong_sym: "R \<in> congruences \<Longrightarrow> R a b \<Longrightarrow> R b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R \<in> congruences; R a b\<rbrakk> \<Longrightarrow> R b a
[PROOF STEP]
by (simp add: congruences_def equivp_symp)