[STATEMENT]
lemma stut_fun3: "\<lbrakk>STUTINV X;STUTINV Y;STUTINV Z\<rbrakk> \<Longrightarrow> STUTINV (f <X,Y,Z>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>STUTINV X; STUTINV Y; STUTINV Z\<rbrakk> \<Longrightarrow> STUTINV f<X, Y, Z>
[PROOF STEP]
by (simp add: stutinv_def)