proposition: Lemma NewObjectAction_Correct: forall p l st_rac2 st_rac2' st_rac3 st_rac3', CorrespondingState p st_rac2 st_rac3 -> NewObjectAction p l st_rac3 = st_rac3' -> Rac2.Assignables.NewObjectAction p l st_rac2 = st_rac2' -> CorrespondingState p st_rac2' st_rac3'.
proof: Proof. intuition. subst. inversion H. split; trivial. subst. simpl in *. destruct H0. split; simpl; trivial. subst. unfold apply_top. destruct H8. destruct fr_rac2 @fresh; destruct fr_rac3 @fresh. split. trivial. trivial. inversion e. inversion e. split; simpl. trivial. intros. destruct n. specialize e0 with 0 d. simpl in e0. unfold ObjSet.Equal in * |- *. split;intros. case_eq(ObjDec.eq_dec l a);intros. apply ObjSet.add_1;trivial. apply ObjSet.add_2;trivial. apply ObjSet.add_3 in H8;trivial. rewrite <- e0;trivial. case_eq(ObjDec.eq_dec l a);intros. apply ObjSet.add_1;trivial. apply ObjSet.add_2;trivial. apply ObjSet.add_3 in H8;trivial. rewrite e0;trivial. specialize e0 with (S n) d. simpl in e0. 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)