proposition: Lemma not_isPivot_direct_FieldInDg: forall p h f dg pivot loc v, isPivot p loc = false -> (direct_FieldInDg_dynamic p h f dg pivot <-> direct_FieldInDg_dynamic p (Heap.update h loc v) f dg pivot).
proof: Proof. intros. apply not_true_iff_false in H. rewrite isPivot_PivotField in H. split; intro. destruct H0. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg; trivial. case_eq (eq_dec loc pivot_loc); intros. rewrite e in H. elim H. split with pivot_fsig pivot_obj pivot_f dg; trivial. rewrite Heap.get_update_old; trivial. destruct H0. split with dg_obj dg_fsig field_obj field_fsig pivot_obj pivot_fsig pivot_f dg; trivial. case_eq (eq_dec loc pivot_loc); intros. rewrite e in H. elim H. split with pivot_fsig pivot_obj pivot_f dg; trivial. rewrite Heap.get_update_old in H3; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)