proposition: Lemma UnfoldDatagroups_rac_intersect_new: forall p h lt fr obj h', Heap.new h p lt = Some (obj, h') -> (forall n, UnfoldDatagroups_rac p h (fst (nth n fr@assignables (LocSet.empty,LocSet.empty))) (snd (nth n fr@assignables (LocSet.empty,LocSet.empty))) [=] UnfoldDatagroups_rac p h' (fst (nth n fr@assignables (LocSet.empty,LocSet.empty))) (snd (nth n fr@assignables (LocSet.empty,LocSet.empty)))).
proof: Proof. intros. generalize n ; clear n. induction fr@assignables. simpl. destruct n; split; rewrite UnfoldDatagroups_rac_def; simpl; intros; destruct H0 as (dg, H0); destruct H0; elim LocSet_empty with dg; trivial. destruct n. simpl. clear IHs. apply UnfoldDatagroups_rac_3 with lt obj;trivial. simpl;trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)