proposition: Lemma rbalS_mapsto l x v r y vy : (rbalS l x v r)@y ↦ vy <-> (Rd l x v r)@y ↦ vy.
proof: Proof. case rbalS_match; intros. - intuition_m. - destmatch; intuition_m; rewrite ?lbal_mapsto in *; intuition_m; rewrite ?makeRed_mapsto in *; intuition_m; apply MapsLeft; rewrite lbal_mapsto; intuition_m. apply MapsLeft. now rewrite makeRed_mapsto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)