proposition: Lemma DoubleNoDup_cons_iff: forall a b l, DoubleNoDup ((a, b) :: l) <-> DoubleNoDup l /\ a <> b /\ ~ InEither a l /\ ~ InEither b l.
proof: Proof. intros. unfold DoubleNoDup, InEither. simpl. destruct (split l) as [l1 l2]. rewrite !NoDup_app_iff, !NoDup_cons_iff, !in_app_iff. simpl. split; intros. - destruct H as [[? ?] [[? ?] ?]]. intuition. + apply (H3 x); right; assumption. + apply (H3 b); left; auto. + apply (H3 a); [left | right]; auto. + apply (H3 b); [right | left]; auto. - destruct H as [[? [? ?]] [? [? ?]]]. apply Decidable.not_or in H3. apply Decidable.not_or in H4. destruct H3, H4. intuition; [subst; contradiction..| apply (H1 x); 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