proposition: Lemma rbal'_in l x r v y : y ∈ (rbal' l x v r) <-> y == x \/ y ∈ l \/ y ∈ r.
proof: Proof. unfold "∈". setoid_rewrite rbal'_mapsto; setoid_rewrite node_mapsto. firstorder. exists v. firstorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)