[STATEMENT]
lemma ctxt_comp_n_funas [simp]:
  "(f, v) \<in> funas_ctxt (C^n) \<Longrightarrow> (f, v) \<in> funas_ctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, v) \<in> funas_ctxt (C ^ n) \<Longrightarrow> (f, v) \<in> funas_ctxt C
[PROOF STEP]
by (induct n arbitrary: C) auto