proposition: Lemma FieldUpdateAction_Correct: forall p loc st_rac st_rac' st_sem st_sem' v, CorrespondingState p st_rac st_sem -> FieldUpdateAction p loc v st_rac = st_rac' -> Sem.Assignables.FieldUpdateAction p loc v st_sem = st_sem' -> CorrespondingState p st_rac' st_sem'.
proof: Proof. intuition. unfold FieldUpdateAction in H0. unfold Sem.Assignables.FieldUpdateAction in H1. subst. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)