[STATEMENT]
lemma tauCases:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi

  assumes "\<tau>.(P) \<longmapsto>\<alpha> \<prec> P'"
  and     "Prop (\<tau>) P"

  shows "Prop \<alpha> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>.P \<longmapsto> \<alpha> \<prec> P'
Prop (\<tau>) P

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
by(cases rule: tauCases') (auto simp add: pi.inject residual.inject)