proposition: Lemma UnfoldDatagroups_rac_3: forall p h h' lt obj pivots assignables, Heap.new h p lt = Some (obj, h') -> UnfoldDatagroups_rac p h pivots assignables [=] UnfoldDatagroups_rac p h' pivots assignables.
proof: Proof. generalize FieldInDg_rac_2. intro. split; intros; rewrite UnfoldDatagroups_rac_def; apply UnfoldDatagroups_rac_def in H1. destruct H1 as (dg, H1). destruct H1. exists dg. split; trivial. clear H1. rewrite UnfoldDatagroup_rac_def in *. specialize H with p h h' lt obj pivots a dg. rewrite <- H; trivial. destruct H1 as (dg, H1). destruct H1. exists dg. split; trivial. clear H1. rewrite UnfoldDatagroup_rac_def in *. specialize H with p h h' lt obj pivots a dg. rewrite H; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)