proposition: Lemma SavePreState_HeapUpdate: forall p h loc a v, EquivAssignableHeap p h (Heap.update h loc v) (fst (SavePreState p h loc a )).
proof: Proof. intros. unfold EquivAssignableHeap. intros. unfold SavePreState in H0. case_eq (LocSet.mem loc (fst a)). intros. rewrite H1 in H0. apply LocSet.mem_2 in H1. assert (loc <> loc0). intuition. elim H0. rewrite <- H2;trivial. symmetry. apply Heap.get_update_old;trivial. intros. rewrite H1 in H0. simpl in H0. assert (loc0 <> loc). auto with *. symmetry. apply Heap.get_update_old. auto. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)