[STATEMENT]
lemma (in encoding_wrt_barbs) indRelTEQ_impl_TRel_respects_barbs:
  fixes TRel :: "('procT \<times> 'procT) set"
  assumes respection: "rel_respects_barbs (indRelTEQ TRel) (STCalWB SWB TWB)"
  shows "rel_respects_barbs TRel TWB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_respects_binary_pred TRel (\<lambda>a. hasBarb a TWB)
[PROOF STEP]
using respection indRelTEQ_impl_TRel_preserves_barbs[where TRel="TRel"]
            indRelTEQ_impl_TRel_reflects_barbs[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred (indRelTEQ TRel) (\<lambda>a. hasBarb a (STCalWB SWB TWB))
rel_preserves_binary_pred (indRelTEQ TRel) (\<lambda>a. hasBarb a (STCalWB SWB TWB)) \<Longrightarrow> rel_preserves_binary_pred TRel (\<lambda>a. hasBarb a TWB)
rel_reflects_binary_pred (indRelTEQ TRel) (\<lambda>b. hasBarb b (STCalWB SWB TWB)) \<Longrightarrow> rel_reflects_binary_pred TRel (\<lambda>b. hasBarb b TWB)

goal (1 subgoal):
 1. rel_respects_binary_pred TRel (\<lambda>a. hasBarb a TWB)
[PROOF STEP]
by blast