proposition: Lemma NoDup_combine_r: forall {A B} (l1: list A) (l2: list B), NoDup l2 -> NoDup (combine l1 l2).
proof: Proof. intros. revert l2 H. induction l1; intros; simpl. 1: constructor. destruct l2; constructor. - intro. apply in_combine_r in H0. apply NoDup_cons_2 in H. contradiction. - apply IHl1. apply NoDup_cons_1 in H. 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