proposition: Lemma makeRed_mapsto m x v : (makeRed m)@x ↦ v <-> m@x ↦ v.
proof: Proof. destruct m; simpl; intuition_m. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)