proposition: Lemma EquivAssignables_2: forall p st loc v, isPivot p loc = false -> EquivAssignables p st st[h:=Heap.update st@h loc v].
proof: Proof. intros. unfold EquivAssignables. simpl. unfold level. rewrite nat_compare_n_n. induction (st@fr@assignables). apply EquivAssignables_base;trivial. apply EquivAssignables_step with a s a s ;trivial. apply UnfoldDatagroups_rac_2. unfold EquivAssignableHeap. intros. apply isPivot_PivotField in H0. assert (loc0 <> loc). intro. rewrite H2 in H0. rewrite H in H0. discriminate H0. symmetry. apply Heap.get_update_old;trivial. auto. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)