proposition: Lemma InEither_dec: forall v l, {InEither v l} + {~ InEither v l}.
proof: Proof. intros. induction l. 1: right; intro; inversion H. destruct a as [v1 v2]. destruct (equiv_dec v v1); unfold equiv in *. - left. rewrite InEither_cons_iff. left. red. simpl. left. assumption. - destruct (equiv_dec v v2); unfold equiv in *. + left. rewrite InEither_cons_iff. left. red. simpl. right. assumption. + destruct IHl; [left | right]. * rewrite InEither_cons_iff. right. assumption. * intro. apply n. clear n. rewrite InEither_cons_iff in H. destruct H; auto. red in H. simpl in H. exfalso. unfold complement in *. destruct H; auto. Defined.
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