proposition: Lemma FieldUpdateCheck_Correct: forall loc p st_rac st_sem, CorrespondingState p st_rac st_sem -> ( FieldUpdateCheck p loc st_rac <-> Sem.Assignables.FieldUpdateCheck p loc st_sem).
proof: Proof. intros loc p stRac stSem H0. destruct H0. inversion_clear H0 as (t1, t2, _, _, _, _, _, _, HC0, HC1, HC2). unfold FieldUpdateCheck; unfold Sem.Assignables.FieldUpdateCheck. unfold CorrespondingFreshAssignables in HC1. destruct HC1 with loc. split; intros. apply H1. intros. rewrite UnfoldDatagroups_def. destruct H2 with n; trivial. left; trivial. destruct H4 as (dg, H4). right. exists dg. rewrite UnfoldDatagroup_def. trivial. destruct H0 with n; trivial. destruct H4 as (fset, H4). left. exists fset. trivial. right. rewrite UnfoldDatagroups_def in H4. destruct H4 as (dg, H4). exists dg. rewrite UnfoldDatagroup_def in H4. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Lia)