proposition: Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 -> (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> bst (merge m1 m2).
proof: Proof. intros m1 m2; functional induction (merge m1 m2); intros; auto; try factornode _x _x0 _x1 _x2 _x3 as m1. apply bal_bst; auto. - generalize (remove_min_bst H0); rewrite e1; simpl in *; auto. - intro; intro. apply H1; auto. generalize (remove_min_in l2 x2 d2 r2 _x4 x); rewrite e1; simpl; intuition auto with relations. - generalize (remove_min_gt_tree H0); rewrite e1; simpl; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int