proposition: Lemma In_map_fst: forall {A B} a b (l: list (A * B)), In (a, b) l -> In a (map fst l).
proof: Proof. intros. assert (exists y, In (a, y) l) by (now exists b). now rewrite <- In_map_fst_iff in H0. 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