[STATEMENT]
lemma typ_of_eta_expand: "typ_of f = Some (\<tau> \<rightarrow> \<tau>') \<Longrightarrow> typ_of (Abs \<tau> (f $ Bv 0)) = Some (\<tau> \<rightarrow> \<tau>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typ_of f = Some (\<tau> \<rightarrow> \<tau>') \<Longrightarrow> typ_of (Abs \<tau> (f $ Bv 0)) = Some (\<tau> \<rightarrow> \<tau>')
[PROOF STEP]
using typ_of1_weaken
[PROOF STATE]
proof (prove)
using this:
typ_of1 ?Ts ?t = Some ?T \<Longrightarrow> typ_of1 (?Ts @ ?Ts') ?t = Some ?T

goal (1 subgoal):
 1. typ_of f = Some (\<tau> \<rightarrow> \<tau>') \<Longrightarrow> typ_of (Abs \<tau> (f $ Bv 0)) = Some (\<tau> \<rightarrow> \<tau>')
[PROOF STEP]
by (fastforce simp add: bind_eq_Some_conv typ_of_def)