[STATEMENT]
lemma heap_read_typedI:
  "\<lbrakk> heap_read h ad al v; \<And>T. P,h \<turnstile> ad@al : T \<Longrightarrow> P,h \<turnstile> v :\<le> T \<rbrakk> \<Longrightarrow> heap_read_typed P h ad al v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_read h ad al v; \<And>T. P,h \<turnstile> ad@al : T \<Longrightarrow> P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> heap_read_typed P h ad al v
[PROOF STEP]
unfolding heap_read_typed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_read h ad al v; \<And>T. P,h \<turnstile> ad@al : T \<Longrightarrow> P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> heap_read h ad al v \<and> (\<forall>T. P,h \<turnstile> ad@al : T \<longrightarrow> P,h \<turnstile> v :\<le> T)
[PROOF STEP]
by blast