proposition: Lemma UnfoldDatagroup_rac_1: forall p h dg f, LocSet.In f (UnfoldDatagroup p h dg) <-> LocSet.In f (UnfoldDatagroup_rac p h LocSet.empty dg).
proof: Proof. intros. split; intros. apply <- UnfoldDatagroup_rac_def. apply UnfoldDatagroup_def in H. rewrite <- FieldInDg_rac_1 in |- *; trivial. apply <- UnfoldDatagroup_def. apply UnfoldDatagroup_rac_def in H. rewrite FieldInDg_rac_1 in |- *; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)