[STATEMENT]
lemma weak_reflection_of_barbs_and_set_of_barbs:
  fixes Rel :: "('proc \<times> 'proc) set"
    and CWB :: "('proc, 'barbs) calculusWithBarbs"
  shows "rel_weakly_reflects_barbs Rel CWB = (\<forall>Barbs. rel_weakly_reflects_barb_set Rel CWB Barbs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_weakly_reflects_barbs Rel CWB = (\<forall>Barbs. rel_weakly_reflects_barb_set Rel CWB Barbs)
[PROOF STEP]
by blast