[STATEMENT]
theorem seqr_post_transfer: "out\<alpha> \<sharp> q \<Longrightarrow> (P ;; (q \<and> R)) = ((P \<and> q\<^sup>-) ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out\<alpha> \<sharp> q \<Longrightarrow> P ;; (q \<and> R) = (P \<and> q\<^sup>-) ;; R
[PROOF STEP]
by (rel_auto)