[STATEMENT]
lemma oconf_init_obj: 
 "\<lbrakk>wf_prog G;  
 (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_prog G; case r of Inl a \<Rightarrow> is_type G (obj_ty obj) | Inr C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<lparr>values := init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r
[PROOF STEP]
apply (auto intro!: oconf_init_obj_lemma unique_fields)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done