[STATEMENT]
lemma subst_bvs_Abs[simp]: "\<forall>x \<in> set args . is_closed x \<Longrightarrow>
  subst_bvs args (Abs T t) = Abs T (subst_bvs1' t 1 args)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set args. is_closed x \<Longrightarrow> subst_bvs args (Abs T t) = Abs T (subst_bvs1' t 1 args)
[PROOF STEP]
using subst_bvs1'_Abs subst_bvs_subst_bvs1'
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set ?args. is_closed x \<Longrightarrow> subst_bvs1' (Abs ?T ?t) ?lev ?args = Abs ?T (subst_bvs1' ?t (Suc ?lev) ?args)
subst_bvs ?s ?t = subst_bvs1' ?t 0 ?s

goal (1 subgoal):
 1. \<forall>x\<in>set args. is_closed x \<Longrightarrow> subst_bvs args (Abs T t) = Abs T (subst_bvs1' t 1 args)
[PROOF STEP]
by auto