proposition: Lemma NewFrame_Correct: forall p m param st_rac1 st_rac2 fr'_rac1 fr'_rac2, CorrespondingState p st_rac1 st_rac2 -> fr'_rac1 = Rac1.NewFrame m param st_rac1 -> fr'_rac2 = NewFrame m param st_rac2 -> CorrespondingState p st_rac1[fr:=fr'_rac1]%rac1 st_rac2[fr:=fr'_rac2].
proof: Proof. intuition. rewrite H0. rewrite H1. unfold NewFrame. unfold Rac1.NewFrame. destruct H. split;trivial. simpl in * |- *. rewrite H9. trivial. simpl. split. destruct H7. simpl. rewrite e. trivial. destruct H7. simpl. destruct n. intros. apply ObjSet.eq_refl. trivial. simpl. split. destruct H8. simpl. rewrite e. trivial. destruct H8. simpl. destruct n. split; rewrite UnfoldDatagroups_def; rewrite UnfoldDatagroups_rac_def;intros. exists a. split. apply LocSetAll_def. rewrite UnfoldDatagroup_rac_def. apply FieldInDg_rac_same;trivial. exists a. split. apply LocSetAll_def. rewrite UnfoldDatagroup_def. apply FieldInDg_same;trivial. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)