[STATEMENT]
lemma val_eq_symm: fixes v1::val and v2::val shows "v1 \<sim> v2 \<Longrightarrow> v2 \<sim> v1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 \<sim> v2 \<Longrightarrow> v2 \<sim> v1
[PROOF STEP]
unfolding val_eq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 \<sqsubseteq> v2 \<and> v2 \<sqsubseteq> v1 \<Longrightarrow> v2 \<sqsubseteq> v1 \<and> v1 \<sqsubseteq> v2
[PROOF STEP]
by blast