proposition: Lemma insert_eq : forall (n : key) (v v' : data) (t1 t2 : btree), search_tree (bnode n v t1 t2) -> INSERT n v' (bnode n v t1 t2) (bnode n v' t1 t2).
proof: Proof. split. inversion 1; eauto with searchtrees. eauto with searchtrees. inversion 1; eauto with searchtrees. inversion H; eauto with searchtrees. Qed.
imports: Relations List ZArith Arith