[STATEMENT]
lemma term_ok'_betapply:
  assumes "term_ok' (sig \<Theta>) f" "term_ok' (sig \<Theta>) u"
  shows "term_ok' (sig \<Theta>) (f \<bullet> u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
proof(cases "f")
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x11 x12. f = Ct x11 x12 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 2. \<And>x21 x22. f = Fv x21 x22 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 3. \<And>x3. f = Bv x3 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 4. \<And>x41 x42. f = Abs x41 x42 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 5. \<And>x51 x52. f = x51 $ x52 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
case (Abs T t)
[PROOF STATE]
proof (state)
this:
f = Abs T t

goal (5 subgoals):
 1. \<And>x11 x12. f = Ct x11 x12 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 2. \<And>x21 x22. f = Fv x21 x22 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 3. \<And>x3. f = Bv x3 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 4. \<And>x41 x42. f = Abs x41 x42 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 5. \<And>x51 x52. f = x51 $ x52 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f = Abs T t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f = Abs T t

goal (1 subgoal):
 1. term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
using assms term_ok'_subst_bv1
[PROOF STATE]
proof (prove)
using this:
f = Abs T t
term_ok' (sig \<Theta>) f
term_ok' (sig \<Theta>) u
\<lbrakk>term_ok' (sig ?\<Theta>) ?f; term_ok' (sig ?\<Theta>) ?u\<rbrakk> \<Longrightarrow> term_ok' (sig ?\<Theta>) (subst_bv1 ?f ?lev ?u)

goal (1 subgoal):
 1. term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
by (simp add: subst_bv_def)
[PROOF STATE]
proof (state)
this:
term_ok' (sig \<Theta>) (f \<bullet> u)

goal (4 subgoals):
 1. \<And>x11 x12. f = Ct x11 x12 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 2. \<And>x21 x22. f = Fv x21 x22 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 3. \<And>x3. f = Bv x3 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
 4. \<And>x51 x52. f = x51 $ x52 \<Longrightarrow> term_ok' (sig \<Theta>) (f \<bullet> u)
[PROOF STEP]
qed (use assms in auto)