proposition: Lemma DoubleNoDup_list_bi_map: forall k v l, DoubleNoDup l -> In (k, v) l -> list_bi_map l k = v /\ list_bi_map l v = k.
proof: Proof. intros. destruct (DoubleNoDup_bi_look_up _ _ _ H H0). unfold list_bi_map. rewrite H1, H2. split; reflexivity. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver