proposition: Lemma lbal_mapsto l x vx r y vy : (lbal l x vx r)@y ↦ vy <-> (Rd l x vx r)@y ↦ vy.
proof: Proof. case lbal_match; intuition_m. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)