proposition: Lemma In_map_fst_iff: forall {A B} a (l: list (A * B)), In a (map fst l) <-> exists b : B, In (a, b) l.
proof: Proof. intros. induction l; simpl. 1: intuition; now destruct H. destruct a0 as [a0 b0]. simpl in *. split; intros. - destruct H. 1: subst; exists b0; now left. rewrite IHl in H. destruct H as [b ?]. exists b. now right. - destruct H as [b ?]. destruct H. 1: inversion H; now left. rewrite IHl. right. now exists b. 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