proposition: Lemma xbindings_sort m j acc : sort lt_key acc -> (forall x p, In x m -> InL p acc -> E.lt (j@x) (fst p)) -> sort lt_key (xbindings m j acc).
proof: Proof. revert j acc. induction m as [|l IHl o r IHr]; simpl; trivial. intros j acc Hacc Hsacc. destruct o as [e|]. - apply IHl;[constructor;[apply IHr; [apply Hacc|]|]|]. + intros. now apply Hsacc. + case_eq (xbindings r j~1 acc); [constructor|]. intros (z,e') q H. constructor. assert (H': InL (z,e') (xbindings r j~1 acc)). { rewrite H. now constructor. } clear H q. rewrite xbindings_spec in H'. destruct H' as [H'|H']. * apply (Hsacc 1 (z,e')); trivial. now exists e. * destruct H' as (x,(->,H)). red. simpl. now apply lt_rev_append. + intros x (y,e') Hx Hy. inversion_clear Hy. rewrite H. simpl. now apply lt_rev_append. rewrite xbindings_spec in H. destruct H as [H|H]. * now apply Hsacc. * destruct H as (z,(->,H)). simpl. now apply lt_rev_append. - apply IHl; [apply IHr; [apply Hacc|]|]. + intros. now apply Hsacc. + intros x (y,e') Hx H. rewrite xbindings_spec in H. destruct H as [H|H]. * now apply Hsacc. * destruct H as (z,(->,H)). simpl. now apply lt_rev_append. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)