proposition: Lemma allkeys_node {elt} P h l x (e:elt) r : Proper (K.eq ==> iff) P -> AllKeys P (Node h l x e r) <-> AllKeys P l /\ P x /\ AllKeys P r.
proof: Proof. unfold AllKeys. setoid_rewrite in_node. firstorder. apply H0; autom. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)