proposition: Lemma nid_in_dec_existsb: forall n l, List.existsb (Nat.eqb n) l = if List.in_dec NId_eq_dec n l then true else false.
proof: Proof. Proof using. intros. case_eq (List.existsb (Nat.eqb n) l); intros. apply List.existsb_exists in H; destruct H as [y[??]]. apply Nat.eqb_eq in H0; subst y. case_eq (List.in_dec NId_eq_dec n l); intros; auto. contradiction. case_eq (List.in_dec NId_eq_dec n l); intros; auto. rewrite <-H. apply List.existsb_exists. exists n; split; auto. apply Nat.eqb_refl. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)