proposition: Lemma get_remove_old_f_uncompat: forall f p pivot st, (forall f_obj f_fsig , f <> Heap.InstanceField f_obj f_fsig) -> get_backlinks st@bl f = get_backlinks (RemoveBacklinks p pivot st) f.
proof: Proof. intros. destruct f. unfold RemoveBacklinks. destruct (Heap.get st @h pivot); trivial. destruct v; trivial. induction (PivotTargets p pivot); trivial. simpl. unfold remove_backlink at 1. destruct Backlinks.get. simpl. unfold get_backlinks. rewrite Backlinks.get_update_old; trivial. intuition. inversion H0; trivial. trivial. elim H with o f. trivial. unfold RemoveBacklinks. destruct (Heap.get st @h pivot); trivial. destruct v; trivial. induction (PivotTargets p pivot); trivial. simpl. unfold remove_backlink at 1. destruct Backlinks.get. simpl. unfold get_backlinks. rewrite Backlinks.get_update_old; trivial. intuition. inversion H0; trivial. 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)