proposition: Lemma mapoL_find l acc x : sort O.ltk (rev l) -> exists y : K.t, y == x /\ findL x (mapoL f l acc) = oelse (obind (findL x (rev l)) (f y)) (findL x acc).
proof: Proof. revert acc. induction l as [|(k,e) l IH]; simpl; intros acc Sl. - now exists x. - rewrite sort_app_key in Sl. destruct Sl as (Sl & _ & AP). apply -> ApartL_rev in AP. destruct (IH (ocons k (f k e) acc) Sl) as (y & Hy & E). clear IH. setoid_rewrite findL_app. setoid_rewrite E. clear E. destruct (findL x (rev l)) eqn:El; simpl in *; auto. + exists y; split; auto. unfold oelse, ocons; destmatch; auto. simpl. destmatch; auto; intros. apply findL_inA in El. rewrite InA_rev in El. apply InA_alt in El. destruct El as ((x',e') & (Hx',_) & IN). compute in Hx'. enough (x' < k) by order. apply (AP (x',e') (k,e)); simpl; auto. + clear l Sl AP El. destruct (f k e) eqn:Fk; simpl; destmatch; intros; firstorder; exists k; simpl; now rewrite Fk. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)