proposition: Lemma Equal_node_iff A (l r l' r' : t A) o o' : Equal (Node l o r) (Node l' o' r') <-> Equal l l' /\ o = o' /\ Equal r r'.
proof: Proof. split. - intros E. repeat split. + intros k. apply (E (k~0)). + apply (E 1). + intros k. apply (E (k~1)). - intros (El & <- & Er) [ | | ]; simpl; auto. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)