proposition: Lemma append_in m1 m2 y : y ∈ (append m1 m2) <-> y ∈ m1 \/ y ∈ m2.
proof: Proof. unfold In. setoid_rewrite append_mapsto. firstorder. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)