proposition: Lemma UnfoldDatagroups_rac_intersect_update: forall p h a loc v, isPivot p loc = false -> (forall n, UnfoldDatagroups_rac p h (fst (nth n a (LocSet.empty,LocSet.empty))) (snd (nth n a (LocSet.empty,LocSet.empty))) [=] UnfoldDatagroups_rac p (Heap.update h loc v) (fst (nth n a (LocSet.empty,LocSet.empty))) (snd (nth n a (LocSet.empty,LocSet.empty)))).
proof: Proof. intros. generalize n;clear n. induction a. 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. clear IHa. apply UnfoldDatagroups_rac_2. unfold EquivAssignableHeap. intros. simpl in H1. elim classic with (loc = loc0);intros. subst. rewrite <- isPivot_PivotField in H0. rewrite H in H0. discriminate H0. rewrite Heap.get_update_old;trivial. simpl;trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)