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