proposition: Lemma makeBlack_in m x : x ∈ (makeBlack m) <-> x ∈ m.
proof: Proof. destruct m; simpl; intuition_in. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)