proposition: Lemma EquivAssignables_3: forall p st lt obj h', Heap.new st@h p lt = Some (obj, h') -> EquivAssignables p st st[h:=h'].
proof: Proof. intros. unfold EquivAssignables. unfold level. rewrite nat_compare_n_n. simpl. induction st @fr @assignables. apply EquivAssignables_base; trivial. apply EquivAssignables_step with a s a s; trivial. apply UnfoldDatagroups_rac_3 with lt obj; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)