proposition: Lemma NewFrame_Correct: forall p m param st_rac2 st_rac3 fr'_rac2 fr'_rac3, CorrespondingState p st_rac2 st_rac3 -> fr'_rac2 = Rac2.NewFrame m param st_rac2 -> fr'_rac3 = NewFrame m param st_rac3 -> CorrespondingState p st_rac2[fr:=fr'_rac2]%rac2 st_rac3[fr:=fr'_rac3].
proof: Proof. intuition. destruct H. split. rewrite H0. rewrite H1. unfold NewFrame. unfold Rac2.NewFrame. destruct H. split; trivial. simpl. rewrite H2. trivial. simpl. split. destruct H9. simpl. rewrite e. trivial. destruct H9. simpl. destruct n. intros. apply ObjSet.eq_refl. trivial. simpl. split. destruct H10. simpl. rewrite e. trivial. destruct H10. simpl. destruct n. intros. split; simpl; apply LocSet.eq_refl. specialize a with (n := n). trivial. simpl; trivial. unfold CorrectBacklinks. intros. split; intros. unfold CorrectBacklinks in H3. simpl. apply H3. rewrite H1 in H4. unfold NewFrame in H4. simpl in H4; trivial. unfold CorrectBacklinks in H3. simpl in H4. apply H3 in H4. rewrite H1. unfold NewFrame. simpl. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)