proposition: Lemma DoubleNoDup_cons_neq: forall v1 v2 l, DoubleNoDup ((v1, v2) :: l) -> ~ InEither v1 l /\ ~ InEither v2 l.
proof: Proof. do 3 intro. revert v1 v2. induction l; intros. 1: intuition. destruct a. specialize (IHl _ _ (DoubleNoDup_cons_tl _ _ H)). destruct IHl. unfold DoubleNoDup in H. simpl in H. unfold InEither in *. simpl. destruct (split l) as [l1 l2]. split. - simpl in H. apply NoDup_cons_2 in H. simpl in *. intro. apply H. destruct H2; auto. right. rewrite in_app_iff in H2 |-* . destruct H2; intuition. - apply NoDup_remove_2 in H. intro. apply H. rewrite in_app_iff in H2 |-* . destruct H2; auto. left. right. assumption. 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