proposition: Lemma DoubleNoDup_app_iff: forall l1 l2, DoubleNoDup (l1 ++ l2) <-> DoubleNoDup l1 /\ DoubleNoDup l2 /\ (forall x, InEither x l1 -> ~ InEither x l2).
proof: Proof. induction l1; simpl; intros. 1: intuition; constructor. destruct a as [a b]. rewrite !DoubleNoDup_cons_iff, !InEither_app_iff, IHl1. clear IHl1. intuition. - apply (H4 x); auto. rewrite InEither_cons_iff in H5. destruct H5; auto. unfold IsEither in H5. simpl in H5. exfalso. destruct H5; subst; contradiction. - apply (H3 x); auto. rewrite InEither_cons_iff. right; assumption. - apply (H3 a); auto. rewrite InEither_cons_iff. left. left. simpl; reflexivity. - apply (H3 b); auto. rewrite InEither_cons_iff. left. right. simpl; reflexivity. 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