[STATEMENT]
lemma s_Let_inv[consumes 2, case_names Let1 Let2, elim]:
  assumes "\<lless> \<pi>, Let e\<^sub>1 x e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
  and     "atom x \<sharp> (e\<^sub>1,\<pi>)"
  and     "e' = e\<^sub>2[e\<^sub>1 / x] \<and> value e\<^sub>1 \<and> \<pi> = \<pi>' \<Longrightarrow> Q"
  and     "\<And>e\<^sub>1'. \<lless> \<pi>, e\<^sub>1 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>1' \<ggreater> \<and> e' = Let e\<^sub>1' x e\<^sub>2 \<and> \<not> value e\<^sub>1 \<Longrightarrow> Q"
  shows   "Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lless>\<pi>, Syntax.Let e\<^sub>1 x e\<^sub>2\<ggreater> m\<rightarrow> \<lless>\<pi>', e'\<ggreater>
atom x \<sharp> (e\<^sub>1, \<pi>)
e' = e\<^sub>2[e\<^sub>1 / x] \<and> value e\<^sub>1 \<and> \<pi> = \<pi>' \<Longrightarrow> Q
\<lless>\<pi>, e\<^sub>1\<ggreater> m\<rightarrow> \<lless>\<pi>', ?e\<^sub>1'\<ggreater> \<and> e' = Syntax.Let ?e\<^sub>1' x e\<^sub>2 \<and> \<not> value e\<^sub>1 \<Longrightarrow> Q

goal (1 subgoal):
 1. Q
[PROOF STEP]
by (auto elim: s_Let_inv')