[STATEMENT]
lemma red_unicity : 
  assumes a: "x \<leadsto> a" 
  and     b: "x \<leadsto> b"
  shows "a=b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
x \<leadsto> a
x \<leadsto> b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
apply (induct arbitrary: b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b. App (Lam [x].t\<^sub>1) t\<^sub>2 \<leadsto> b \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 2. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (erule whr_inv_auto(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b xa t\<^sub>1'. \<lbrakk>[x].t\<^sub>1 = [xa].t\<^sub>1'; b = t\<^sub>1'[xa::=t\<^sub>2]\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 2. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 3. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b xa t\<^sub>1'. [x].t\<^sub>1 = [xa].t\<^sub>1' \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = t\<^sub>1'[xa::=t\<^sub>2]
 2. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 3. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (rule subst_fun_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b xa t\<^sub>1'. [x].t\<^sub>1 = [xa].t\<^sub>1' \<Longrightarrow> [x].t\<^sub>1 = [xa].t\<^sub>1'
 2. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 3. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 2. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (erule whr_inv_auto(6))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b x t\<^sub>1''. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; t\<^sub>1 = Lam [x].t\<^sub>1''; b = t\<^sub>1''[x::=t\<^sub>2]\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
 2. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b t\<^sub>1''. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; b = App t\<^sub>1'' t\<^sub>2; t\<^sub>1 \<leadsto> t\<^sub>1''\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (blast)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done