proposition: Lemma InEither_map_iff: forall v (l: list (A * A)), InEither v l <-> In v (map fst l) \/ In v (map snd l).
proof: Proof. intros. unfold InEither. destruct (split l) eqn:? . rewrite in_app_iff, map_fst_split, map_snd_split, Heqp. now simpl. 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