proposition: Lemma findL_inA {elt} x e (l : klist elt) : findL x l = Some e -> InA O.eqke (x,e) l.
proof: Proof. induction l as [|(k,v) l IH]; simpl; try easy. destmatch; intro E; auto. intros [= ->]; auto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)