proposition: Lemma look_up_not_In: forall l v, ~ In v (map fst l) <-> look_up l v = None.
proof: Proof. induction l; intros; simpl. 1: intuition. destruct a as [k v']. simpl. split; intros. - apply Decidable.not_or in H. destruct H. destruct (equiv_dec k v); unfold equiv in *; [contradiction | now apply IHl]. - destruct (equiv_dec k v). 1: inversion H. rewrite <- IHl in H. intro. unfold equiv, complement in c. destruct H0; contradiction. 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