proposition: Lemma SavePreState_2: forall p h a pivot v, (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 pivot v) (fst (nth n (map (SavePreState p h pivot) a) (LocSet.empty,LocSet.empty))) (snd (nth n (map (SavePreState p h pivot) a) (LocSet.empty,LocSet.empty)))).
proof: Proof. induction a. simpl. destruct n; split; rewrite UnfoldDatagroups_rac_def; simpl; intros; destruct H as (dg, H); destruct H; elim LocSet_empty with dg; trivial. destruct n. simpl. clear IHa. destruct a as (pivots, assignables). simpl. pose proof (SavePreState_1 p h pivot pivots assignables) as H. simpl in H. generalize UnfoldDatagroups_rac_2. intro. specialize H0 with p h (Heap.update h pivot v) (fst (SavePreState p h pivot (pivots, assignables) )) (snd (SavePreState p h pivot (pivots, assignables) )). generalize SavePreState_HeapUpdate. intro. apply H0 in H1. generalize H1. generalize H. apply LocSet.eq_trans. simpl. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)