proposition: Lemma In_InEither: forall v1 v2 l, In (v1, v2) l -> InEither v1 l /\ InEither v2 l.
proof: Proof. do 3 intro. revert v1 v2. induction l; intros. 1: inversion H. simpl in H. destruct H. - subst. rewrite !InEither_cons_iff. unfold IsEither. simpl. intuition. - apply IHl in H. destruct H. rewrite !InEither_cons_iff. intuition. 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