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