proposition: Lemma LocDict_get_some: forall bl f pivot ams, LocDict.get (get_backlinks bl f) pivot = Some ams -> exists ad, Backlinks.get bl f = Some ad.
proof: Proof. intros. unfold get_backlinks in H. case_eq (Backlinks.get bl f);intros. exists v;trivial. rewrite H0 in H. rewrite LocDict.get_empty in H. inversion H. 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)