[STATEMENT]
lemma vappend_transfer[transfer_rule]: 
  includes lifting_syntax
  shows "(cr_vfsequence ===> cr_vfsequence ===> cr_vfsequence) 
    (\<lambda>xs ys. vappend ys xs) append"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_vfsequence ===> cr_vfsequence ===> cr_vfsequence) (\<lambda>xs ys. ys @\<^sub>\<circ> xs) (@)
[PROOF STEP]
by (intro rel_funI, unfold cr_vfsequence_def) (simp add: vappend_def)