[STATEMENT]
lemma mgu_new: 
  "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mgu t1 t2 = Some u; new_tv n t1; new_tv n t2\<rbrakk> \<Longrightarrow> new_tv n u
[PROOF STEP]
by (meson UnE mgu_free new_tv_def subsetD)