proposition: Lemma findL_find {elt} x (m : t elt) `{!Ok m} : findL x (bindings m) = find x m.
proof: Proof. apply eq_option_alt. intro e. rewrite findL_inA_iff by now apply bindings_spec2. rewrite find_spec by auto. apply bindings_spec1. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)