[STATEMENT]
lemma (in encoding) enc_respects_pred_iff_indRel_respects_pred:
  fixes Pred :: "('procS, 'procT) Proc \<Rightarrow> bool"
  shows "enc_respects_pred Pred = rel_respects_pred indRel Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enc_respects_pred Pred = rel_respects_pred indRel Pred
[PROOF STEP]
using enc_respects_pred_iff_indRelR_respects_pred[where Pred="Pred"]
            indRel_respects_pred_iff_indRelR_respects_pred[where Pred="Pred"]
[PROOF STATE]
proof (prove)
using this:
enc_respects_pred Pred = rel_respects_pred indRelR Pred
rel_respects_pred indRel Pred = rel_respects_pred indRelR Pred

goal (1 subgoal):
 1. enc_respects_pred Pred = rel_respects_pred indRel Pred
[PROOF STEP]
by simp