proposition: Lemma DoubleNoDup_bi_look_up: forall k v l, DoubleNoDup l -> In (k, v) l -> bi_look_up l k = Some v /\ bi_look_up l v = Some k.
proof: Proof. do 3 intro. induction l; intros. 1: inversion H0. assert (a = (k, v) \/ a <> (k, v)). { destruct a; destruct (equiv_dec a k); destruct (equiv_dec a0 v); unfold equiv in *; unfold complement in *; simpl in *; subst; [left; reflexivity | right; intro; apply c; inversion H1; reflexivity..]. } destruct H1. - subst. simpl. apply DoubleNoDup_cons_hd in H. destruct (equiv_dec k k); intuition. destruct (equiv_dec k v); intuition. destruct (equiv_dec v v); intuition. - destruct a. simpl. destruct (equiv_dec a k); unfold equiv in *. + exfalso. subst a. apply H1. f_equal. eapply DoubleNoDup_In_fst_eq; eauto. simpl. left; reflexivity. + destruct (equiv_dec a0 k); unfold equiv in *. * exfalso. subst a0. eapply (DoubleNoDup_In_fst_snd_impsb _ a); eauto. simpl. left; reflexivity. * destruct (equiv_dec a v); unfold equiv in *. -- exfalso. subst a. eapply (DoubleNoDup_In_fst_snd_impsb _ k a0 v); eauto. simpl. left; reflexivity. -- destruct (equiv_dec a0 v); unfold equiv in *. ++ exfalso. subst. apply H1. f_equal. eapply DoubleNoDup_In_snd_eq; eauto. simpl. left; reflexivity. ++ apply IHl. 1: eapply DoubleNoDup_cons_tl; eauto. simpl in H0. destruct H0; auto. contradiction. 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