proposition: Lemma bindings_above x (e:elt) (m:t elt) : m < x <-> bindings m < [(x,e)].
proof: Proof. split. - intros H p q Hp [<-|[ ]]. simpl. apply H. exists (p#2). rewrite <- bindings_spec1. apply In_InA; ok. now destruct p. - intros H y (v,M). rewrite <- bindings_spec1, InA_alt in M. destruct M as (p & E & IN). redk. destruct E as (->,->). apply (H _ (x,e)); simpl; auto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)