proposition: Lemma UnfoldDatagroups_rac_1: forall p h dgs f, LocSet.In f (UnfoldDatagroups p h dgs) <-> LocSet.In f (UnfoldDatagroups_rac p h LocSet.empty dgs).
proof: Proof. intros. split;intros. apply <- UnfoldDatagroups_rac_def. apply UnfoldDatagroups_def in H. destruct H as [dg H]. destruct H. exists dg. split;trivial. rewrite <- UnfoldDatagroup_rac_1;trivial. apply <- UnfoldDatagroups_def. apply UnfoldDatagroups_rac_def in H. destruct H as [dg H]. destruct H. exists dg. split;trivial. rewrite UnfoldDatagroup_rac_1;trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)