proposition: Lemma In_look_up: forall l v a, look_up l v = Some a -> In v (map fst l) /\ In a (map snd l).
proof: Proof. induction l; intros; simpl in *. 1: inversion H. destruct a as [k v']. simpl. destruct (equiv_dec k v); unfold equiv in *. - inversion H. subst. intuition. - apply IHl in H. destruct H. split; now right. 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