proposition: Lemma list_bi_map_In: forall l x, InEither x l -> exists k v, In (k, v) l /\ ((x = k /\ list_bi_map l x = v) \/ (x = v /\ list_bi_map l x = k)).
proof: Proof. induction l; intros. 1: inversion H. destruct (IsEither_dec x a). - destruct a. exists a, a0. simpl. split. 1: left; reflexivity. red in i. simpl in i. destruct i; subst; [left | right]; split; try reflexivity; unfold list_bi_map; simpl. + destruct (equiv_dec a a); [| exfalso; apply c]; reflexivity. + destruct (equiv_dec a a0). 1: intuition. destruct (equiv_dec a0 a0); [| exfalso; apply c0]; reflexivity. - rewrite InEither_cons_iff in H. destruct H. 1: contradiction. specialize (IHl _ H). destruct IHl as [k [v [? ?]]]. exists k, v. split. + simpl. right; assumption. + destruct a. unfold IsEither in n. simpl in n. apply Decidable.not_or in n. destruct n. unfold list_bi_map in *. simpl. destruct (equiv_dec a x); unfold equiv in *. 1: exfalso; intuition. destruct (equiv_dec a0 x); unfold equiv in *. 1: exfalso; intuition. 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