proposition: Lemma FieldUpdateAction_Correct: forall p loc st_rac1 v st_rac1' st_rac2 st_rac2', CorrespondingState p st_rac1 st_rac2 -> FieldUpdateAction p loc v st_rac2 = st_rac2' -> Rac1.Assignables.FieldUpdateAction p loc v st_rac1 = st_rac1' -> CorrespondingState p st_rac1'[h:=Heap.update st_rac1@h loc v]%rac1 st_rac2'[h:=Heap.update st_rac2@h loc v].
proof: Proof. intuition. inversion H. subst. unfold Rac1.Assignables.FieldUpdateAction. unfold FieldUpdateAction. case_eq (isPivot p loc); intro. split; simpl; trivial. split. rewrite map_length. destruct H9. trivial. generalize SavePreState_2. intros. specialize H1 with p st_rac2 @h st_rac2 @fr@assignables loc v n. destruct H9. generalize H1. specialize e0 with n. generalize e0. apply LocSet.eq_trans. rewrite H10. trivial. split; trivial. simpl. split. destruct H9;trivial. generalize UnfoldDatagroups_rac_intersect_update. intro. intros. specialize H1 with p st_rac2 @h st_rac2 @fr@assignables loc v n. apply H1 in H0. clear H1. destruct H9. specialize e0 with n. generalize H0. generalize e0. apply LocSet.eq_trans. simpl. rewrite H10. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)