proposition: Lemma UnfoldDatagroups_rac_2: forall p h h' pivots assignables, EquivAssignableHeap p h h' pivots -> UnfoldDatagroups_rac p h pivots assignables [=] UnfoldDatagroups_rac p h' pivots assignables.
proof: Proof. unfold EquivAssignableHeap. split; intros; apply <- UnfoldDatagroups_rac_def; apply UnfoldDatagroups_rac_def in H0. destruct H0 as (dg, H0). exists dg. destruct H0. split; trivial. apply <- UnfoldDatagroup_rac_def. apply UnfoldDatagroup_rac_def in H1. clear assignables H0. induction H1. apply FieldInDg_rac_step with dg'; trivial. apply FieldInDg_rac_static; trivial. apply FieldInDg_rac_dynamic with pivot. destruct H0. apply direct_FieldInDg_dynamic_def with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg; trivial. rewrite <- H in |- *; trivial. split with pivot_fsig pivot_obj pivot_f dg; trivial. trivial. subst. apply FieldInDg_rac_same; trivial. destruct H0 as (dg, H0). exists dg. destruct H0. split; trivial. apply <- UnfoldDatagroup_rac_def. apply UnfoldDatagroup_rac_def in H1. clear assignables H0. induction H1. apply FieldInDg_rac_step with dg'; trivial. apply FieldInDg_rac_static; trivial. apply FieldInDg_rac_dynamic with pivot. destruct H0. apply direct_FieldInDg_dynamic_def with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg; trivial. rewrite H in |- *; trivial. split with pivot_fsig pivot_obj pivot_f dg; trivial. trivial. subst. apply FieldInDg_rac_same; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)