proposition: Lemma SavePreState_3: forall p loc st v, let (a, a') := level st @fr @assignables (map (SavePreState p st @h loc) st @fr @assignables) in EquivAssignables_ind p st@h (Heap.update st@h loc v) a a'.
proof: Proof. intros. unfold level. rewrite map_length. rewrite nat_compare_n_n. induction st@fr@assignables. simpl. apply EquivAssignables_base;trivial. simpl. apply EquivAssignables_step with a s (SavePreState p st@h loc a) (map (SavePreState p st@h loc) s); trivial. rewrite map_length;trivial. pose proof (SavePreState_1 p st@h loc (fst a) (snd a)) as H. simpl in H. replace ((fst a), (snd a)) with a in H by (destruct a;trivial). generalize UnfoldDatagroups_rac_2. intros. specialize H0 with p st@h (Heap.update st@h loc v) (fst (SavePreState p st@h loc a )) (snd (SavePreState p st@h loc a )). generalize SavePreState_HeapUpdate. intros. apply H0 in H1. generalize H1. generalize H. apply LocSet.eq_trans. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)