proposition: Lemma mem_1 : forall m x, In x m -> mem x m = true.
proof: Proof. unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto. apply (is_bst m). Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia