proposition: Lemma append_in (l r : t elt) x : x ∈ (append l r) <-> x ∈ l \/ x ∈ r.
proof: Proof. unfold "∈". setoid_rewrite append_mapsto. firstorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)