proposition: Lemma bindings_aux_sort m acc `{!Ok m} : sort ltk acc -> (forall x e y, InA eqke (x,e) acc -> y ∈ m -> y < x) -> sort ltk (bindings_aux acc m).
proof: Proof. revert acc. induction m as [ | h l Hl y e r Hr ]; intros acc; simpl; intuition. invok. apply Hl; auto. - constructor. + apply Hr; eautom. + clear Hl Hr. apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') Hy'. apply bindings_aux_mapsto in Hy'. change (y < y'). intuition; eautom. - clear Hl Hr. intros x e' y' Hx Hy'. rewrite InA_cons in Hx. redk. destruct Hx as [(Hx,->)|Hx]. + order. + apply bindings_aux_mapsto in Hx. intuition. order. eautom. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)