proposition: Lemma bindings_below x (e:elt) (m:t elt) : x < m <-> [(x,e)] < bindings m.
proof: Proof. split. - intros H p q [<-|[ ]] Hq. simpl. apply H. exists (q#2). rewrite <- bindings_spec1. apply In_InA; ok. now destruct q. - 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)