[STATEMENT]
lemma Apps_Var_neq_Apps_beta[simp, THEN not_sym, simp]:
  "\<langle>xT\<rangle> \<bullet> ss \<noteq> \<Lambda>\<langle>T\<rangle> r \<cdot> s \<bullet> ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>xT\<rangle> \<bullet> ss \<noteq> \<Lambda>\<langle>T\<rangle> r \<cdot> s \<bullet> ts
[PROOF STEP]
by (metis Apps_Var_neq_Apps_Abs Apps_append Apps_snoc eq_Apps_conv(9))