proposition: Lemma findL_inA_iff {elt} x e (l : klist elt) : sort O.ltk l -> (findL x l = Some e <-> InA O.eqke (x,e) l).
proof: Proof. intros Sl. split; [apply findL_inA| ]. revert Sl. induction l as [|(k,v) l IH]; simpl; try easy. inversion_clear 1. rewrite InA_cons. redk. intros [(E,->)|IN]. - destmatch; intros; auto || order. - destmatch; intros; auto. assert (LT : O.ltk (k,v) (x,e)) by (eapply SortA_InfA_InA with (eqA:=O.eqke); ok). compute in LT. order. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)