Replacing the old version of "functional induction" with the new one.

The old version is, for now, still available by prefixing any command/tactic with Old/old (eg. old functional induction ...).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8881 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 430 insertions, 396 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 17be9405c..af5cee4fa 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -469,7 +469,7 @@ Ltac omega_bal := match goal with
 
 (** * Insertion *)
 
-Fixpoint add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s with 
+Function add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s with 
    | Leaf => Node (Leaf _) x e (Leaf _) 1
    | Node l y e' r h => 
       match X.compare x y with
@@ -482,17 +482,17 @@ Fixpoint add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s wi
 Lemma add_avl_1 :  forall elt (m:t elt) x e, avl m -> 
  avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1.
 Proof. 
- intros elt m x e; functional induction add elt x e m; intros; inv avl; simpl in *.
+ intros elt m x e; functional induction (add x e m); intros; inv avl; simpl in *.
  intuition; try constructor; simpl; auto; try omega_max.
  (* LT *)
- destruct H; auto.
+ destruct IHt; auto.
  split.
  apply bal_avl; auto; omega_max.
  omega_bal.
  (* EQ *)
  intuition; omega_max.
  (* GT *)
- destruct H; auto.
+ destruct IHt; auto.
  split.
  apply bal_avl; auto; omega_max.
  omega_bal.
@@ -507,12 +507,12 @@ Hint Resolve add_avl.
 Lemma add_in : forall elt (m:t elt) x y e, avl m -> 
  (In y (add x e m) <-> X.eq y x \/ In y m).
 Proof.
- intros elt m x y e; functional induction add elt x e m; auto; intros.
+ intros elt m x y e; functional induction (add x e m); auto; intros.
  intuition_in.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (H H1); intuition_in.
+ rewrite (IHt H2); intuition_in.
  (* EQ *)  
  inv avl.
  firstorder_in.
@@ -520,30 +520,30 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (H H2); intuition_in.
+ rewrite (IHt H3); intuition_in.
 Qed.
 
 Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m).
 Proof. 
- intros elt m x e; functional induction add elt x e m; 
+ intros elt m x e; functional induction (add x e m); 
    intros; inv bst; inv avl; auto; apply bal_bst; auto.
  (* lt_tree -> lt_tree (add ...) *)
- red; red in H4.
+ red; red in H5.
  intros.
- rewrite (add_in x y0 e H0) in H1.
+ rewrite (add_in x y0 e H1) in H2.
  intuition.
  eauto.
  (* gt_tree -> gt_tree (add ...) *)
- red; red in H4.
+ red; red in H5.
  intros.
- rewrite (add_in x y0 e H6) in H1.
+ rewrite (add_in x y0 e H7) in H2.
  intuition.
  apply lt_eq with x; auto.
 Qed.
 
 Lemma add_1 : forall elt (m:t elt) x y e, avl m -> X.eq x y -> MapsTo y e (add x e m).
 Proof. 
- intros elt m x y e; functional induction add elt x e m; 
+ intros elt m x y e; functional induction (add x e m); 
    intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; eauto.
 Qed. 
 
@@ -574,25 +574,26 @@ Qed.
   for [t=Leaf], we pre-unpack [t] (and forget about [h]). 
 *)
  
-Fixpoint remove_min (elt:Set)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := 
+Function remove_min (elt:Set)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := 
   match l with 
     | Leaf => (r,(x,e))
-    | Node ll lx le lr lh => let (l',m) := remove_min ll lx le lr in (bal l' x e r, m)
+    | Node ll lx le lr lh => let (l',m) := (remove_min ll lx le lr : t elt*(key*elt)) in (bal l' x e r, m)
   end.
 
 Lemma remove_min_avl_1 : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> 
  avl (fst (remove_min l x e r)) /\ 
  0 <= height (Node l x e r h) - height (fst (remove_min l x e r)) <= 1.
 Proof.
- intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros.
+ intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv avl; simpl in *; split; auto.
  avl_nns; omega_max.
  (* l = Node *)
- inversion_clear H0.
- destruct (H lh); auto.
+ inversion_clear H1.
+ destruct (IHp lh); auto.
  split; simpl in *. 
- apply bal_avl; auto; omega_max.
- omega_bal.
+ rewrite_all H0. simpl in *.
+ apply bal_avl; subst;auto; omega_max.
+ rewrite_all H0;simpl in *;omega_bal.
 Qed.
 
 Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> 
@@ -605,16 +606,17 @@ Lemma remove_min_in : forall elt (l:t elt) x e r h y, avl (Node l x e r h) ->
  (In y (Node l x e r h) <-> 
   X.eq y (fst (snd (remove_min l x e r))) \/ In y (fst (remove_min l x e r))).
 Proof.
- intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros.
+ intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in.
  (* l = Node *)
- inversion_clear H0.
- generalize (remove_min_avl H1).
- rewrite H_eq_0; simpl; intros.
+ inversion_clear H1.
+ generalize (remove_min_avl H2).
+ 
+ rewrite_all H0; simpl; intros.
  rewrite bal_in; auto.
- generalize (H lh y H1).
+ generalize (IHp lh y H2).
  intuition.
- inversion_clear H8; intuition.
+ inversion_clear H9; intuition.
 Qed.
 
 Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> 
@@ -622,49 +624,50 @@ Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h
    ((X.eq y (fst (snd (remove_min l x e r))) /\ e' = (snd (snd (remove_min l x e r))))
     \/ MapsTo y e' (fst (remove_min l x e r)))).
 Proof.
- intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros.
+ intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  intuition_in; subst; auto.
  (* l = Node *)
- inversion_clear H0.
- generalize (remove_min_avl H1).
- rewrite H_eq_0; simpl; intros.
+ inversion_clear H1.
+ generalize (remove_min_avl H2).
+ rewrite_all H0; simpl; intros.
  rewrite bal_mapsto; auto; unfold create.
- destruct (H lh y e').
+ simpl in *;destruct (IHp lh y e').
  auto.
  intuition.
- inversion_clear H3; intuition.
- inversion_clear H10; intuition.
+ inversion_clear H4; intuition.
+ inversion_clear H11; intuition.
 Qed.
 
 Lemma remove_min_bst : forall elt (l:t elt) x e r h, 
  bst (Node l x e r h) -> avl (Node l x e r h) -> bst (fst (remove_min l x e r)).
 Proof.
- intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros.
+ intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H0; inversion_clear H1.
+ inversion_clear H1; inversion_clear H2.
  apply bal_bst; auto.
- firstorder.
+ rewrite_all H0;simpl in *;firstorder.
  intro; intros.
- generalize (remove_min_in y H0).
- rewrite H_eq_0; simpl.
+ generalize (remove_min_in y H1).
+ rewrite_all H0; simpl in *.
  destruct 1.
- apply H4; intuition.
+ apply H5; intuition.
 Qed.
 
 Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, 
  bst (Node l x e r h) -> avl (Node l x e r h) -> 
  gt_tree (fst (snd (remove_min l x e r))) (fst (remove_min l x e r)).
 Proof.
- intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros.
+ intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H0; inversion_clear H1.
+ inversion_clear H1; inversion_clear H2.
  intro; intro.
- generalize (H lh H2 H0); clear H8 H7 H.
- generalize (remove_min_avl H0).
- generalize (remove_min_in (fst m) H0).
- rewrite H_eq_0; simpl; intros.
- rewrite (bal_in x e y H7 H6) in H1.
- destruct H.
+ rewrite_all H0;simpl in *.
+ generalize (IHp lh H3 H1); clear H9 H8 IHp.
+ generalize (remove_min_avl H1).
+ generalize (remove_min_in (fst m) H1).
+ rewrite H0; simpl; intros.
+ rewrite (bal_in x e y H9 H7) in H2.
+ destruct H8.
  firstorder.
  apply lt_eq with x; auto.
  apply X.lt_trans with x; auto.
@@ -677,13 +680,13 @@ Qed.
   [|height t1 - height t2| <= 2].
 *)
 
-Definition merge elt (s1 s2 : t elt) :=  match s1,s2 with 
+Function merge (elt:Set) (s1 s2 : t elt) : tree elt :=  match s1,s2 with 
   | Leaf, _ => s2 
   | _, Leaf => s1
   | _, Node l2 x2 e2 r2 h2 => 
-        let (s2',m) := remove_min l2 x2 e2 r2 in 
-        let (x,e) := m in 
-        bal s1 x e s2'
+    match remove_min l2 x2 e2 r2 with 
+      (s2',(x,e)) => bal s1 x e s2'
+    end
 end.
 
 Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> 
@@ -691,12 +694,13 @@ Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 ->
  avl (merge s1 s2) /\ 
  0<= height (merge s1 s2) - max (height s1) (height s2) <=1.
 Proof.
- intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros.
+ intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros;subst.
  split; auto; avl_nns; omega_max.
+ destruct _x;try contradiction;clear H1.
  split; auto; avl_nns; simpl in *; omega_max.
- generalize (remove_min_avl_1 H0).
- rewrite H_eq_1; simpl; destruct 1.
- rewrite H_eq_2; simpl.
+ destruct _x;try contradiction;clear H1.
+ generalize (remove_min_avl_1 H4).
+rewrite H2; simpl;destruct 1.
  split.
  apply bal_avl; auto.
  simpl; omega_max.
@@ -712,49 +716,53 @@ Qed.
 Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (In y (merge s1 s2) <-> In y s1 \/ In y s2).
 Proof. 
- intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros.
+ intros elt s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
  intuition_in.
  intuition_in.
- rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2.
- replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H_eq_1; auto].
+ destruct _x;try contradiction;clear H1.
+(*  rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *)
+ replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
  rewrite bal_in; auto.
- generalize (remove_min_avl H2); rewrite H_eq_1; simpl; auto.
- generalize (remove_min_in y0 H2); rewrite H_eq_1; simpl; intro.
- rewrite H3; intuition.
+ generalize (remove_min_avl H4); rewrite H2; simpl; auto.
+ generalize (remove_min_in y H4); rewrite H2; simpl; intro.
+ rewrite H1; intuition.
 Qed.
 
 Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
   (MapsTo y e (merge s1 s2) <-> MapsTo y e s1 \/ MapsTo y e s2).
 Proof.
- intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros.
+ intros elt s1 s2; functional induction (@merge elt s1 s2); subst; simpl in *; intros.
  intuition_in.
  intuition_in.
- rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2.
- replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H_eq_1; auto].
+ destruct _x;try contradiction;clear H1.
+ replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
  rewrite bal_mapsto; auto; unfold create.
- generalize (remove_min_avl H2); rewrite H_eq_1; simpl; auto.
- generalize (remove_min_mapsto y0 e0 H2); rewrite H_eq_1; simpl; intro.
- rewrite H3; intuition (try subst; auto).
- inversion_clear H3; intuition.
+ generalize (remove_min_avl H4); rewrite H2; simpl; auto.
+ generalize (remove_min_mapsto y e0 H4); rewrite H2; simpl; intro.
+ rewrite H1; intuition (try subst; auto).
+ inversion_clear H1; intuition.
 Qed.
 
 Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (forall y1 y2 : key, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (merge s1 s2). 
 Proof.
- intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros; auto.
- rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2.
+ intros elt s1 s2; functional induction (@merge elt s1 s2); subst;simpl in *; intros; auto.
+
  apply bal_bst; auto.
- generalize (remove_min_bst H1); rewrite H_eq_1; simpl in *; auto.
+ destruct _x;try contradiction.
+ generalize (remove_min_bst H3); rewrite H2; simpl in *; auto.
+ destruct _x;try contradiction.
  intro; intro.
- apply H3; auto.
- generalize (remove_min_in x H2); rewrite H_eq_1; simpl; intuition.
- generalize (remove_min_gt_tree H1); rewrite H_eq_1; simpl; auto.
+ apply H5; auto.
+ generalize (remove_min_in x H4); rewrite H2; simpl; intuition.
+ destruct _x;try contradiction.
+ generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto.
 Qed. 
 
 (** * Deletion *)
 
-Fixpoint remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with 
+Function remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with 
   | Leaf => Leaf _
   | Node l y e r h =>
       match X.compare x y with
@@ -767,22 +775,22 @@ Fixpoint remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with
 Lemma remove_avl_1 : forall elt (s:t elt) x, avl s -> 
  avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
 Proof.
- intros elt s x; functional induction remove elt x s; simpl; intros.
+ intros elt s x; functional induction (@remove elt x s); subst;simpl; intros.
  split; auto; omega_max.
  (* LT *)
  inv avl.
- destruct (H H1).
+ destruct (IHt H1).
  split. 
  apply bal_avl; auto.
  omega_max.
  omega_bal.
  (* EQ *)
  inv avl. 
- generalize (merge_avl_1 H0 H1 H2).
+ generalize (merge_avl_1 H1 H2 H3).
  intuition omega_max.
  (* GT *)
  inv avl.
- destruct (H H2).
+ destruct (IHt H2).
  split. 
  apply bal_avl; auto.
  omega_max.
@@ -798,32 +806,32 @@ Hint Resolve remove_avl.
 Lemma remove_in : forall elt (s:t elt) x y, bst s -> avl s -> 
  (In y (remove x s) <-> ~ X.eq y x /\ In y s).
 Proof.
- intros elt s x; functional induction remove elt x s; simpl; intros.
+ intros elt s x; functional induction (@remove elt x s); simpl; intros.
  intuition_in.
  (* LT *)
- inv avl; inv bst; clear H_eq_0.
+ inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (H y0 H1); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H2); intuition; [ order | order | intuition_in ].
  (* EQ *)
- inv avl; inv bst; clear H_eq_0.
+ inv avl; inv bst; clear H0.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
- elim H9; eauto.
+ elim H10; eauto.
  (* GT *)
- inv avl; inv bst; clear H_eq_0.
+ inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (H y0 H6); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H7); intuition; [ order | order | intuition_in ].
 Qed.
 
 Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s).
 Proof. 
- intros elt s x; functional induction remove elt x s; simpl; intros.
+ intros elt s x; functional induction (@remove elt x s); subst;simpl; intros.
  auto.
  (* LT *)
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in x y0 H1) in H0; auto.
- destruct H0; eauto.
+ rewrite (remove_in x y0 H1) in H; auto.
+ destruct H; eauto.
  (* EQ *)
  inv avl; inv bst.
  apply merge_bst; eauto.
@@ -831,8 +839,8 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in x y0 H6) in H0; auto.
- destruct H0; eauto.
+ rewrite (remove_in x y0 H6) in H; auto.
+ destruct H; eauto.
 Qed.
 
 Lemma remove_1 : forall elt (m:t elt) x y, bst m -> avl m -> X.eq x y -> ~ In y (remove x m).
@@ -911,7 +919,7 @@ Qed.
 (** The [mem] function is deciding appartness. It exploits the [bst] property
     to achieve logarithmic complexity. *)
 
-Fixpoint mem (x:key)(m:t elt) { struct m } : bool := 
+Function mem (x:key)(m:t elt) { struct m } : bool := 
    match m with 
      |  Leaf => false 
      |  Node l y e r _ => match X.compare x y with 
@@ -925,7 +933,7 @@ Implicit Arguments mem.
 Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true.
 Proof. 
  intros s x.
- functional induction mem x s; inversion_clear 1; auto.
+ functional induction (mem x s); inversion_clear 1; auto.
  intuition_in.
  intuition_in; firstorder; absurd (X.lt x y); eauto.
  intuition_in; firstorder; absurd (X.lt y x); eauto.
@@ -934,10 +942,10 @@ Qed.
 Lemma mem_2 : forall s x, mem x s = true -> In x s. 
 Proof. 
  intros s x. 
- functional induction mem x s; firstorder; intros; try discriminate.
+ functional induction (mem x s); firstorder; intros; try discriminate.
 Qed.
 
-Fixpoint find (x:key)(m:t elt) { struct m } : option elt := 
+Function find (x:key)(m:t elt) { struct m } : option elt := 
    match m with 
      |  Leaf => None 
      |  Node l y e r _ => match X.compare x y with 
@@ -950,7 +958,7 @@ Fixpoint find (x:key)(m:t elt) { struct m } : option elt :=
 Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.
 Proof. 
  intros m x e.
- functional induction find x m; inversion_clear 1; auto.
+ functional induction (find x m); inversion_clear 1; auto.
  intuition_in.
  intuition_in; firstorder; absurd (X.lt x y); eauto.
  intuition_in; auto.
@@ -962,7 +970,7 @@ Qed.
 Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
 Proof. 
  intros m x.
- functional induction find x m; firstorder; intros; try discriminate.
+ functional induction (find x m); subst;firstorder; intros; try discriminate.
  inversion H; subst; auto.
 Qed.
 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 4b2761f10..128ed45d2 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -96,7 +96,7 @@ Qed.
 
 (** * [mem] *)
 
-Fixpoint mem (k : key) (s : t elt) {struct s} : bool :=
+Function mem (k : key) (s : t elt) {struct s} : bool :=
  match s with
   | nil => false
   | (k',_) :: l =>
@@ -110,33 +110,33 @@ Fixpoint mem (k : key) (s : t elt) {struct s} : bool :=
 Lemma mem_1 : forall m (Hm:Sort m) x, In x m -> mem x m = true.
 Proof.  
  intros m Hm x; generalize Hm; clear Hm.      
- functional induction mem x m;intros sorted belong1;trivial.
+ functional induction (mem x m);intros sorted belong1;trivial.
  
- inversion belong1. inversion H.
+ inversion belong1. inversion H0.
  
- absurd (In k ((k', e) :: l));try assumption.
- apply Sort_Inf_NotIn with e;auto.
+ absurd (In x ((k', _x) :: l));try assumption.
+ apply Sort_Inf_NotIn with _x;auto.
 
- apply H.
+ apply IHb.
  elim (sort_inv sorted);auto.
  elim (In_inv belong1);auto.
  intro abs.
- absurd (X.eq k k');auto.
+ absurd (X.eq x k');auto.
 Qed. 
 
 Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. 
 Proof.
  intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo.
- functional induction mem x m; intros sorted hyp;try ((inversion hyp);fail).
- exists e; auto. 
- induction H; auto.
- exists x; auto.
+ functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail).
+ exists _x; auto. 
+ induction IHb; auto.
+ exists x0; auto.
  inversion_clear sorted; auto.
 Qed.
 
 (** * [find] *)
 
-Fixpoint find (k:key) (s: t elt) {struct s} : option elt :=
+Function find (k:key) (s: t elt) {struct s} : option elt :=
  match s with
   | nil => None
   | (k',x)::s' => 
@@ -150,31 +150,31 @@ Fixpoint find (k:key) (s: t elt) {struct s} : option elt :=
 Lemma find_2 :  forall m x e, find x m = Some e -> MapsTo x e m.
 Proof.
  intros m x. unfold PX.MapsTo.
- functional induction find x m;simpl;intros e' eqfind; inversion eqfind; auto.
+ functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto.
 Qed.
 
 Lemma find_1 :  forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. 
 Proof.
  intros m Hm x e; generalize Hm; clear Hm; unfold PX.MapsTo.
- functional induction find x m;simpl; subst; try clear H_eq_1.
+ functional induction (find x m);simpl; subst; try clear H_eq_1.
 
  inversion 2.
 
  inversion_clear 2.
- compute in H0; destruct H0; order.
- generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order.
+ clear H0;compute in H1; destruct H1;order.
+ clear H0;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H1)); compute; order.
 
- inversion_clear 2.
+ clear H0;inversion_clear 2.
  compute in H0; destruct H0; intuition congruence. 
  generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order.
  
- do 2 inversion_clear 1; auto.
- compute in H3; destruct H3; order.
+ clear H0; do 2 inversion_clear 1; auto.
+ compute in H2; destruct H2; order.
 Qed.
 
 (** * [add] *)
 
-Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt :=
+Function add (k : key) (x : elt) (s : t elt) {struct s} : t elt :=
  match s with
   | nil => (k,x) :: nil
   | (k',y) :: l =>
@@ -189,7 +189,7 @@ Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
 Proof.
  intros m x y e; generalize y; clear y.
  unfold PX.MapsTo.
- functional induction add x e m;simpl;auto.
+ functional induction (add x e m);simpl;auto.
 Qed.
 
 Lemma add_2 : forall m x y e e', 
@@ -197,25 +197,29 @@ Lemma add_2 : forall m x y e e',
 Proof.
  intros m x  y e e'. 
  generalize y e; clear y e; unfold PX.MapsTo.
- functional induction add x e' m;simpl;auto; clear H_eq_1.
- intros y' e' eqky';  inversion_clear 1; destruct H0; simpl in *.
+ functional induction (add x e' m) ;simpl;auto;  clear H0.
+ subst;auto.
+
+ intros y' e'' eqky';  inversion_clear 1; destruct H1; simpl in *.
  order.
  auto.
  auto.
- intros y' e' eqky'; inversion_clear 1; intuition.
+ intros y' e'' eqky'; inversion_clear 1; intuition.
 Qed.
   
+
 Lemma add_3 : forall m x y e e',
   ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
 Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
- functional induction add x e' m;simpl; intros.
- apply (In_inv_3 H0); compute; auto.
- apply (In_inv_3 H0); compute; auto.
- constructor 2; apply (In_inv_3 H0); compute; auto. 
- inversion_clear H1; auto.
+ functional induction (add x e' m);simpl; intros.
+ apply (In_inv_3 H1); compute; auto.
+ subst s;apply (In_inv_3 H2); compute; auto.
+ constructor 2; apply (In_inv_3 H2); compute; auto. 
+ inversion_clear H2; auto.
 Qed.
 
+
 Lemma add_Inf : forall (m:t elt)(x x':key)(e e':elt), 
   Inf (x',e') m -> ltk (x',e') (x,e) -> Inf (x',e') (add x e m).
 Proof.
@@ -242,7 +246,7 @@ Qed.
 
 (** * [remove] *)
 
-Fixpoint remove (k : key) (s : t elt) {struct s} : t elt :=
+Function remove (k : key) (s : t elt) {struct s} : t elt :=
  match s with
   | nil => nil
   | (k',x) :: l =>
@@ -256,30 +260,36 @@ Fixpoint remove (k : key) (s : t elt) {struct s} : t elt :=
 Lemma remove_1 : forall m (Hm:Sort m) x y, X.eq x y -> ~ In y (remove x m).
 Proof.
  intros m Hm x y; generalize Hm; clear Hm.
- functional induction remove x m;simpl;intros;subst;try clear H_eq_1.
+ functional induction (remove x m);simpl;intros;subst.
  
  red; inversion 1; inversion H1.
 
- apply Sort_Inf_NotIn with x; auto.
- constructor; compute; order.
+ apply Sort_Inf_NotIn with x0; auto.
+ clear H0;constructor; compute; order.
  
- inversion_clear Hm.
- apply Sort_Inf_NotIn with x; auto. 
- apply Inf_eq with (k',x);auto; compute; apply X.eq_trans with k; auto.
+ clear H0;inversion_clear Hm.
+ apply Sort_Inf_NotIn with x0; auto. 
+ apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto.
 
- inversion_clear Hm.
- assert (notin:~ In y (remove k l)) by auto.
- intros (x0,abs).
+ clear H0;inversion_clear Hm.
+ assert (notin:~ In y (remove x l)) by auto.
+ intros (x1,abs).
  inversion_clear abs. 
- compute in H3; destruct H3; order.
- apply notin; exists x0; auto.
+ compute in H2; destruct H2; order.
+ apply notin; exists x1; auto.
 Qed.
 
+
 Lemma remove_2 : forall m (Hm:Sort m) x y e, 
   ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
- functional induction remove x m;auto; try clear H_eq_1.
+ functional induction (remove x m);subst;auto; 
+   match goal with 
+     | [H: X.compare _ _ = _ |- _ ] => clear H
+     | _ => idtac
+   end.
+
  inversion_clear 3; auto.
  compute in H1; destruct H1; order.
  
@@ -290,7 +300,7 @@ Lemma remove_3 : forall m (Hm:Sort m) x y e,
   MapsTo y e (remove x m) -> MapsTo y e m.
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
- functional induction remove x m;auto.
+ functional induction (remove x m);subst;auto.
  inversion_clear 1; inversion_clear 1; auto.
 Qed.
 
@@ -341,8 +351,7 @@ Qed.
 
 (** * [fold] *)
 
-Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A :=
-  fun acc => 
+Function fold (A:Set)(f:key->elt->A->A)(m:t elt) (acc:A) {struct m} :  A :=
   match m with
    | nil => acc
    | (k,e)::m' => fold f m' (f k e acc)
@@ -351,12 +360,12 @@ Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A :=
 Lemma fold_1 : forall m (A:Set)(i:A)(f:key->elt->A->A),
   fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 Proof. 
- intros; functional induction fold A f m i; auto.
+ intros; functional induction (fold f m i); auto.
 Qed.
 
 (** * [equal] *)
 
-Fixpoint equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool := 
+Function equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool := 
   match m, m' with 
    | nil, nil => true
    | (x,e)::l, (x',e')::l' => 
@@ -375,56 +384,52 @@ Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp,
   Equal cmp m m' -> equal cmp m m' = true. 
 Proof. 
  intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
- functional induction equal cmp m m'; simpl; auto; unfold Equal;
- intuition; subst; try clear H_eq_3.
+ functional induction (equal cmp m m'); simpl; subst;auto; unfold Equal;
+ intuition; subst;   match goal with 
+     | [H: X.compare _ _ = _ |- _ ] => clear H
+     | _ => idtac
+   end.
 
- destruct p as (k,e).
- destruct (H0 k).
- destruct H2.
- exists e; auto.
- inversion H2.
 
- destruct (H0 x).
- destruct H.
- exists e; auto.
- inversion H.
 
- destruct (H0 x).
- assert (In x ((x',e')::l')). 
-  apply H; auto.
-  exists e; auto.
- destruct (In_inv H3).
- order.
- inversion_clear Hm'.
- assert (Inf (x,e) l').
- apply Inf_lt with (x',e'); auto.
- elim (Sort_Inf_NotIn H5 H7 H4).
- 
- assert (cmp e e' = true).
+ assert (cmp_e_e':cmp e e' = true).
   apply H2 with x; auto.
- rewrite H0; simpl.
- apply H; auto.
+ rewrite cmp_e_e'; simpl.
+ apply IHb; auto.
  inversion_clear Hm; auto.
  inversion_clear Hm'; auto.
  unfold Equal; intuition.
- destruct (H1 k).
+ destruct (H0 k).
  assert (In k ((x,e) ::l)).
-  destruct H3 as (e'', hyp); exists e''; auto.
- destruct (In_inv (H4 H6)); auto.
+  destruct H as (e'', hyp); exists e''; auto.
+ destruct (In_inv (H1 H4)); auto.
  inversion_clear Hm.
- elim (Sort_Inf_NotIn H8 H9).
- destruct H3 as (e'', hyp); exists e''; auto.
+ elim (Sort_Inf_NotIn H6 H7).
+ destruct H as (e'', hyp); exists e''; auto.
  apply MapsTo_eq with k; auto; order.
- destruct (H1 k).
+ destruct (H0 k).
  assert (In k ((x',e') ::l')).
-  destruct H3 as (e'', hyp); exists e''; auto.
- destruct (In_inv (H5 H6)); auto.
+  destruct H as (e'', hyp); exists e''; auto.
+ destruct (In_inv (H3 H4)); auto.
  inversion_clear Hm'.
- elim (Sort_Inf_NotIn H8 H9).
- destruct H3 as (e'', hyp); exists e''; auto.
+ elim (Sort_Inf_NotIn H6 H7).
+ destruct H as (e'', hyp); exists e''; auto.
  apply MapsTo_eq with k; auto; order.
  apply H2 with k; destruct (eq_dec x k); auto.
 
+
+ destruct (X.compare x x'); try contradiction;clear H2.
+ destruct (H0 x).
+ assert (In x ((x',e')::l')). 
+  apply H; auto.
+  exists e; auto.
+ destruct (In_inv H3).
+ order.
+ inversion_clear Hm'.
+ assert (Inf (x,e) l').
+ apply Inf_lt with (x',e'); auto.
+ elim (Sort_Inf_NotIn H5 H7 H4).
+
  destruct (H0 x').
  assert (In x' ((x,e)::l)). 
   apply H2; auto.
@@ -435,43 +440,70 @@ Proof.
  assert (Inf (x',e') l).
   apply Inf_lt with (x,e); auto.
  elim (Sort_Inf_NotIn H5 H7 H4).
+
+ destruct _x;
+ destruct _x0;try contradiction.
+ 
+ clear H1;destruct p as (k,e).
+ destruct (H0 k).
+ destruct H1.
+ exists e; auto.
+ inversion H1.
+
+ destruct p as (x,e).
+ destruct (H0 x).
+ destruct H.
+ exists e; auto.
+ inversion H.
+
+ destruct p;destruct p0;contradiction.
 Qed.
 
+
 Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, 
   equal cmp m m' = true -> Equal cmp m m'.
 Proof.
  intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
- functional induction equal cmp m m'; simpl; auto; unfold Equal; 
-  intuition; try discriminate; subst; try clear H_eq_3; 
-  try solve [inversion H0]; destruct (andb_prop _ _ H0); clear H0; 
-  inversion_clear Hm; inversion_clear Hm'.
-
- destruct (H H0 H5 H3).
- destruct (In_inv H1).
+ functional induction (equal cmp m m'); simpl; subst;auto; unfold Equal; 
+  intuition; try discriminate; subst; match goal with 
+     | [H: X.compare _ _ = _ |- _ ] => clear H
+     | _ => idtac
+   end. 
+
+ inversion H0.
+
+ inversion_clear Hm;inversion_clear Hm'.
+ destruct (andb_prop _ _ H); clear H. 
+ destruct (IHb H1 H3 H6).
+ destruct (In_inv H0).
  exists e'; constructor; split; trivial; apply X.eq_trans with x; auto.
- destruct (H7 k).
- destruct (H10 H9) as (e'',hyp).
+ destruct (H k).
+ destruct (H9 H8) as (e'',hyp).
  exists e''; auto.
 
- destruct (H H0 H5 H3).
- destruct (In_inv H1).
+ inversion_clear Hm;inversion_clear Hm'.
+ destruct (andb_prop _ _ H); clear H. 
+ destruct (IHb H1 H3 H6).
+ destruct (In_inv H0).
  exists e; constructor; split; trivial; apply X.eq_trans with x'; auto.
- destruct (H7 k).
- destruct (H11 H9) as (e'',hyp).
+ destruct (H k).
+ destruct (H10 H8) as (e'',hyp).
  exists e''; auto.
 
- destruct (H H0 H6 H4).
- inversion_clear H1.
- destruct H10; simpl in *; subst.
+ inversion_clear Hm;inversion_clear Hm'.
+ destruct (andb_prop _ _ H); clear H. 
+ destruct (IHb H1 H4 H7).
+ inversion_clear H0.
+ destruct H9; simpl in *; subst.
  inversion_clear H2. 
- destruct H10; simpl in *; subst; auto.
- elim (Sort_Inf_NotIn H6 H7).
+ destruct H9; simpl in *; subst; auto.
+ elim (Sort_Inf_NotIn H4 H5).
  exists e'0; apply MapsTo_eq with k; auto; order.
  inversion_clear H2. 
- destruct H1; simpl in *; subst; auto.
- elim (Sort_Inf_NotIn H0 H5).
- exists e1; apply MapsTo_eq with k; auto; order.
- apply H9 with k; auto.
+ destruct H0; simpl in *; subst; auto.
+ elim (Sort_Inf_NotIn H1 H3).
+ exists e0; apply MapsTo_eq with k; auto; order.
+ apply H8 with k; auto.
 Qed. 
 
 (** This lemma isn't part of the spec of [Equal], but is used in [FMapAVL] *)
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index dc034bf83..415e0c113 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -91,7 +91,7 @@ Qed.
 
 (** * [mem] *)
 
-Fixpoint mem (k : key) (s : t elt) {struct s} : bool :=
+Function mem (k : key) (s : t elt) {struct s} : bool :=
   match s with
    | nil => false
    | (k',_) :: l => if X.eq_dec k k' then true else mem k l
@@ -100,30 +100,30 @@ Fixpoint mem (k : key) (s : t elt) {struct s} : bool :=
 Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true.
 Proof.
  intros m Hm x; generalize Hm; clear Hm.      
- functional induction mem x m;intros NoDup belong1;trivial.
- inversion belong1. inversion H.
+ functional induction (mem x m);intros NoDup belong1;trivial.
+ inversion belong1. inversion H0.
  inversion_clear NoDup.
  inversion_clear belong1.
  inversion_clear H3.
  compute in H4; destruct H4.
  elim H; auto.
- apply H0; auto.
- exists x; auto.
+ apply IHb; auto.
+ exists x0; auto.
 Qed. 
 
 Lemma mem_2 : forall m (Hm:NoDupA m) x, mem x m = true -> In x m. 
 Proof.
  intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo.
- functional induction mem x m; intros NoDup hyp; try discriminate.
- exists e; auto. 
+ functional induction (mem x m); intros NoDup hyp; try discriminate.
+ exists _x; auto. 
  inversion_clear NoDup.
- destruct H0; auto.
- exists x; auto.
+ destruct IHb; auto.
+ exists x0; auto.
 Qed.
 
 (** * [find] *)
 
-Fixpoint find (k:key) (s: t elt) {struct s} : option elt :=
+Function find (k:key) (s: t elt) {struct s} : option elt :=
   match s with
    | nil => None
    | (k',x)::s' => if X.eq_dec k k' then Some x else find k s'
@@ -132,23 +132,23 @@ Fixpoint find (k:key) (s: t elt) {struct s} : option elt :=
 Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
 Proof.
  intros m x. unfold PX.MapsTo.
- functional induction find x m;simpl;intros e' eqfind; inversion eqfind; auto.
+ functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto.
 Qed.
 
 Lemma find_1 : forall m (Hm:NoDupA m) x e, 
   MapsTo x e m -> find x m = Some e. 
 Proof.
  intros m Hm x e; generalize Hm; clear Hm; unfold PX.MapsTo.
- functional induction find x m;simpl; subst; try clear H_eq_1.
+ functional induction (find x m);simpl; subst; try clear H_eq_1.
 
  inversion 2.
 
  do 2 inversion_clear 1.
  compute in H3; destruct H3; subst; trivial.
- elim H0; apply InA_eqk with (k,e); auto.
+ elim H; apply InA_eqk with (x,e); auto.
 
  do 2 inversion_clear 1; auto.
- compute in H4; destruct H4; elim H; auto.
+ compute in H3; destruct H3; elim _x; auto.
 Qed.
 
 (* Not part of the exported specifications, used later for [combine]. *)
@@ -166,7 +166,7 @@ Qed.
 
 (** * [add] *)
 
-Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt :=
+Function add (k : key) (x : elt) (s : t elt) {struct s} : t elt :=
   match s with
    | nil => (k,x) :: nil
    | (k',y) :: l => if X.eq_dec k k' then (k,x)::l else (k',y)::add k x l
@@ -175,28 +175,28 @@ Fixpoint add (k : key) (x : elt) (s : t elt) {struct s} : t elt :=
 Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
 Proof.
  intros m x y e; generalize y; clear y; unfold PX.MapsTo.
- functional induction add x e m;simpl;auto.
+ functional induction (add x e m);simpl;auto.
 Qed.
 
 Lemma add_2 : forall m x y e e', 
   ~ X.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
 Proof.
  intros m x  y e e'; generalize y e; clear y e; unfold PX.MapsTo.
- functional induction add x e' m;simpl;auto.
- intros y' e' eqky';  inversion_clear 1.
- destruct H1; simpl in *.
+ functional induction (add x e' m);simpl;auto.
+ intros y' e'' eqky';  inversion_clear 1.
+ destruct H2; simpl in *.
  elim eqky'; apply X.eq_trans with k'; auto.
  auto.
- intros y' e' eqky'; inversion_clear 1; intuition.
+ intros y' e'' eqky'; inversion_clear 1; intuition.
 Qed.
   
 Lemma add_3 : forall m x y e e',
   ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
 Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
- functional induction add x e' m;simpl;auto.
- intros; apply (In_inv_3 H0); auto.
- constructor 2; apply (In_inv_3 H1); auto.
+ functional induction (add x e' m);simpl;auto.
+ intros; apply (In_inv_3 H1); auto.
+ constructor 2; apply (In_inv_3 H2); auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -204,12 +204,12 @@ Lemma add_3' : forall m x y e e',
   ~ X.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m. 
 Proof.
  intros m x y e e'. generalize y e; clear y e.
- functional induction add x e' m;simpl;auto.
+ functional induction (add x e' m);simpl;auto.
  inversion_clear 2.
- compute in H1; elim H; auto.
- inversion H1. 
- constructor 2; inversion_clear H1; auto.
  compute in H2; elim H0; auto.
+ inversion H2. 
+ constructor 2; inversion_clear H2; auto.
+ compute in H3; elim H1; auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -257,7 +257,7 @@ Qed.
 
 (** * [remove] *)
 
-Fixpoint remove (k : key) (s : t elt) {struct s} : t elt :=
+Function remove (k : key) (s : t elt) {struct s} : t elt :=
   match s with
    | nil => nil
    | (k',x) :: l => if X.eq_dec k k' then l else (k',x) :: remove k l
@@ -266,23 +266,23 @@ Fixpoint remove (k : key) (s : t elt) {struct s} : t elt :=
 Lemma remove_1 : forall m (Hm:NoDupA m) x y, X.eq x y -> ~ In y (remove x m).
 Proof.
  intros m Hm x y; generalize Hm; clear Hm.
- functional induction remove x m;simpl;intros;auto.
+ functional induction (remove x m);simpl;intros;auto.
 
- red; inversion 1; inversion H1.
+ red; inversion 1; inversion H2.
 
  inversion_clear Hm.
  subst.
- swap H1.
- destruct H3 as (e,H3); unfold PX.MapsTo in H3.
+ swap H2.
+ destruct H as (e,H); unfold PX.MapsTo in H.
  apply InA_eqk with (y,e); auto.
- compute; apply X.eq_trans with k; auto.
+ compute; apply X.eq_trans with x; auto.
   
  intro H2.
  destruct H2 as (e,H2); inversion_clear H2.
  compute in H3; destruct H3.
- elim H; apply X.eq_trans with y; auto.
+ elim _x; apply X.eq_trans with y; auto.
  inversion_clear Hm.
- elim (H0 H4 H1).
+ elim (IHt0 H4 H1).
  exists e; auto.
 Qed.
   
@@ -290,10 +290,10 @@ Lemma remove_2 : forall m (Hm:NoDupA m) x y e,
   ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
- functional induction remove x m;auto.
+ functional induction (remove x m);auto.
  inversion_clear 3; auto.
- compute in H2; destruct H2.
- elim H0; apply X.eq_trans with k'; auto.
+ compute in H3; destruct H3.
+ elim H1; apply X.eq_trans with k'; auto.
   
  inversion_clear 1; inversion_clear 2; auto.
 Qed.
@@ -302,7 +302,7 @@ Lemma remove_3 : forall m (Hm:NoDupA m) x y e,
   MapsTo y e (remove x m) -> MapsTo y e m.
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
- functional induction remove x m;auto.
+ functional induction (remove x m);auto.
  do 2 inversion_clear 1; auto.
 Qed.
 
@@ -310,7 +310,7 @@ Lemma remove_3' : forall m (Hm:NoDupA m) x y e,
   InA eqk (y,e) (remove x m) -> InA eqk (y,e) m.
 Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
- functional induction remove x m;auto.
+ functional induction (remove x m);auto.
  do 2 inversion_clear 1; auto.
 Qed.
 
@@ -347,8 +347,7 @@ Qed.
 
 (** * [fold] *)
 
-Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A :=
-  fun acc => 
+Function fold (A:Set)(f:key->elt->A->A)(m:t elt) (acc : A) {struct m} :  A :=
   match m with
    | nil => acc
    | (k,e)::m' => fold f m' (f k e acc)
@@ -357,7 +356,7 @@ Fixpoint fold (A:Set)(f:key->elt->A->A)(m:t elt) {struct m} : A -> A :=
 Lemma fold_1 : forall m (A:Set)(i:A)(f:key->elt->A->A),
   fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 Proof. 
- intros; functional induction fold A f m i; auto.
+ intros; functional induction (@fold A f m i); auto.
 Qed.
 
 (** * [equal] *)
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 3c6f49394..5b912f8b2 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -287,7 +287,7 @@ Qed.
 (** The [mem] function is deciding appartness. It exploits the [bst] property
     to achieve logarithmic complexity. *)
 
-Fixpoint mem (x:elt)(s:t) { struct s } : bool := 
+Function mem (x:elt)(s:t) { struct s } : bool := 
    match s with 
      |  Leaf => false 
      |  Node l y r _ => match X.compare x y with 
@@ -300,7 +300,7 @@ Fixpoint mem (x:elt)(s:t) { struct s } : bool :=
 Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true.
 Proof. 
  intros s x.
- functional induction mem x s; inversion_clear 1; auto.
+ functional induction (mem x s); inversion_clear 1; auto.
  inversion_clear 1.
  inversion_clear 1; auto; absurd (X.lt x y); eauto.
  inversion_clear 1; auto; absurd (X.lt y x); eauto.
@@ -309,7 +309,7 @@ Qed.
 Lemma mem_2 : forall s x, mem x s = true -> In x s. 
 Proof. 
  intros s x. 
- functional induction mem x s; auto; intros; try discriminate.
+ functional induction (mem x s); auto; intros; try discriminate.
 Qed.
 
 (** * Singleton set *)
@@ -472,7 +472,7 @@ Ltac omega_bal := match goal with
 
 (** * Insertion *)
 
-Fixpoint add (x:elt)(s:t) { struct s } : t := match s with 
+Function add (x:elt)(s:t) { struct s } : t := match s with 
    | Leaf => Node Leaf x Leaf 1
    | Node l y r h => 
       match X.compare x y with
@@ -485,17 +485,17 @@ Fixpoint add (x:elt)(s:t) { struct s } : t := match s with
 Lemma add_avl_1 :  forall s x, avl s -> 
  avl (add x s) /\ 0 <= height (add x s) - height s <= 1.
 Proof. 
- intros s x; functional induction add x s; intros; inv avl; simpl in *.
+ intros s x; functional induction (add x s); subst;intros; inv avl; simpl in *.
  intuition; try constructor; simpl; auto; try omega_max.
  (* LT *)
- destruct H; auto.
+ destruct IHt; auto.
  split.
  apply bal_avl; auto; omega_max.
  omega_bal.
  (* EQ *)
  intuition; omega_max.
  (* GT *)
- destruct H; auto.
+ destruct IHt; auto.
  split.
  apply bal_avl; auto; omega_max.
  omega_bal.
@@ -510,12 +510,12 @@ Hint Resolve add_avl.
 Lemma add_in : forall s x y, avl s -> 
  (In y (add x s) <-> X.eq y x \/ In y s).
 Proof.
- intros s x; functional induction add x s; auto; intros.
+ intros s x; functional induction (add x s); auto; intros.
  intuition_in.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (H y0 H1); intuition_in.
+ rewrite (IHt y0 H2); intuition_in.
  (* EQ *)  
  inv avl.
  intuition.
@@ -523,24 +523,24 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (H y0 H2); intuition_in.
+ rewrite (IHt y0 H3); intuition_in.
 Qed.
 
 Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s).
 Proof. 
- intros s x; functional induction add x s; auto; intros.
+ intros s x; functional induction (add x s); auto; intros.
  inv bst; inv avl; apply bal_bst; auto.
  (* lt_tree -> lt_tree (add ...) *)
- red; red in H4.
+ red; red in H5.
  intros.
- rewrite (add_in l x y0 H0) in H1.
+ rewrite (add_in l x y0 H1) in H2.
  intuition.
  eauto.
  inv bst; inv avl; apply bal_bst; auto.
  (* gt_tree -> gt_tree (add ...) *)
- red; red in H4.
+ red; red in H5.
  intros.
- rewrite (add_in r x y0 H6) in H1.
+ rewrite (add_in r x y0 H7) in H2.
  intuition.
  apply MX.lt_eq with x; auto.
 Qed.
@@ -688,22 +688,22 @@ Qed.
   for [t=Leaf], we pre-unpack [t] (and forget about [h]). 
 *)
  
-Fixpoint remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt := 
+Function remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt := 
   match l with 
     | Leaf => (r,x)
-    | Node ll lx lr lh => let (l',m) := remove_min ll lx lr in (bal l' x r, m)
+    | Node ll lx lr lh => let (l',m) := (remove_min ll lx lr : t*elt) in (bal l' x r, m)
   end.
 
 Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) -> 
  avl (fst (remove_min l x r)) /\ 
  0 <= height (Node l x r h) - height (fst (remove_min l x r)) <= 1.
 Proof.
- intros l x r; functional induction remove_min l x r; simpl in *; intros.
+ intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
  inv avl; simpl in *; split; auto.
  avl_nns; omega_max.
  (* l = Node *)
- inversion_clear H0.
- destruct (H lh); auto.
+ inversion_clear H.
+ rewrite H0 in IHp;simpl in IHp;destruct (IHp lh); auto.
  split; simpl in *. 
  apply bal_avl; auto; omega_max.
  omega_bal.
@@ -719,29 +719,30 @@ Lemma remove_min_in : forall l x r h y, avl (Node l x r h) ->
  (In y (Node l x r h) <-> 
   X.eq y (snd (remove_min l x r)) \/ In y (fst (remove_min l x r))).
 Proof.
- intros l x r; functional induction remove_min l x r; simpl in *; intros.
+ intros l x r; functional induction (remove_min l x r); simpl in *; intros.
  intuition_in.
  (* l = Node *)
- inversion_clear H0.
- generalize (remove_min_avl ll lx lr lh H1).
- rewrite H_eq_0; simpl; intros.
+ inversion_clear H1.
+ generalize (remove_min_avl ll lx lr lh H2).
+ rewrite H0; simpl; intros.
  rewrite bal_in; auto.
- generalize (H lh y H1).
+ rewrite H0 in IHp;generalize (IHp lh y H2).
  intuition.
- inversion_clear H8; intuition.
+ inversion_clear H9; intuition.
 Qed.
 
 Lemma remove_min_bst : forall l x r h, 
  bst (Node l x r h) -> avl (Node l x r h) -> bst (fst (remove_min l x r)).
 Proof.
- intros l x r; functional induction remove_min l x r; simpl in *; intros.
+ intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
  inv bst; auto.
- inversion_clear H0; inversion_clear H1.
+ inversion_clear H; inversion_clear H1.
+ rewrite_all H0;simpl in *.
  apply bal_bst; auto.
  firstorder.
  intro; intros.
- generalize (remove_min_in ll lx lr lh y H0).
- rewrite H_eq_0; simpl.
+ generalize (remove_min_in ll lx lr lh y H).
+ rewrite H0; simpl.
  destruct 1.
  apply H4; intuition.
 Qed.
@@ -750,16 +751,16 @@ Lemma remove_min_gt_tree : forall l x r h,
  bst (Node l x r h) -> avl (Node l x r h) -> 
  gt_tree (snd (remove_min l x r)) (fst (remove_min l x r)).
 Proof.
- intros l x r; functional induction remove_min l x r; simpl in *; intros.
+ intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
  inv bst; auto.
- inversion_clear H0; inversion_clear H1.
+ inversion_clear H; inversion_clear H1.
  intro; intro.
- generalize (H lh H2 H0); clear H8 H7 H.
- generalize (remove_min_avl ll lx lr lh H0).
- generalize (remove_min_in ll lx lr lh m H0).
- rewrite H_eq_0; simpl; intros.
- rewrite (bal_in l' x r y H7 H6) in H1.
- destruct H.
+ generalize (IHp lh H2 H); clear H8 H7 IHp.
+ generalize (remove_min_avl ll lx lr lh H).
+ generalize (remove_min_in ll lx lr lh m H).
+ rewrite H0; simpl; intros.
+ rewrite (bal_in l' x r y H8 H6) in H1.
+ destruct H7.
  firstorder.
  apply MX.lt_eq with x; auto.
  apply X.lt_trans with x; auto.
@@ -772,7 +773,7 @@ Qed.
   [|height t1 - height t2| <= 2].
 *)
 
-Definition merge s1 s2 :=  match s1,s2 with 
+Function merge (s1 s2 :t) : t:=  match s1,s2 with 
   | Leaf, _ => s2 
   | _, Leaf => s1
   | _, Node l2 x2 r2 h2 => 
@@ -784,11 +785,12 @@ Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 ->
  avl (merge s1 s2) /\ 
  0<= height (merge s1 s2) - max (height s1) (height s2) <=1.
 Proof.
- intros s1 s2; functional induction merge s1 s2; simpl in *; intros.
+ intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
  split; auto; avl_nns; omega_max.
  split; auto; avl_nns; simpl in *; omega_max.
+ destruct _x;try contradiction;clear H1.
  generalize (remove_min_avl_1 l2 x2 r2 h2 H0).
- rewrite H_eq_1; simpl; destruct 1.
+ rewrite H2; simpl; destruct 1.
  split.
  apply bal_avl; auto.
  simpl; omega_max.
@@ -804,32 +806,34 @@ Qed.
 Lemma merge_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (In y (merge s1 s2) <-> In y s1 \/ In y s2).
 Proof. 
- intros s1 s2; functional induction merge s1 s2; simpl in *; intros.
+ intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros.
  intuition_in.
  intuition_in.
- replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H_eq_1; auto].
+ destruct _x;try contradiction;clear H1.
+ replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H2; auto].
  rewrite bal_in; auto.
- generalize (remove_min_avl l2 x2 r2 h2); rewrite H_eq_1; simpl; auto.
- generalize (remove_min_in l2 x2 r2 h2 y); rewrite H_eq_1; simpl; intro.
- rewrite H3; intuition.
+ generalize (remove_min_avl l2 x2 r2 h2); rewrite H2; simpl; auto.
+ generalize (remove_min_in l2 x2 r2 h2 y); rewrite H2; simpl; intro.
+ rewrite H1; intuition.
 Qed.
 
 Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (merge s1 s2). 
 Proof.
- intros s1 s2; functional induction merge s1 s2; simpl in *; intros; auto.
+ intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto.
+ destruct _x;try contradiction;clear H1.
  apply bal_bst; auto.
- generalize (remove_min_bst l2 x2 r2 h2); rewrite H_eq_1; simpl in *; auto.
+ generalize (remove_min_bst l2 x2 r2 h2); rewrite H2; simpl in *; auto.
  intro; intro.
- apply H3; auto.
- generalize (remove_min_in l2 x2 r2 h2 m); rewrite H_eq_1; simpl; intuition.
- generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H_eq_1; simpl; auto.
+ apply H5; auto.
+ generalize (remove_min_in l2 x2 r2 h2 m); rewrite H2; simpl; intuition.
+ generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H2; simpl; auto.
 Qed. 
 
 (** * Deletion *)
 
-Fixpoint remove (x:elt)(s:tree) { struct s } : t := match s with 
+Function remove (x:elt)(s:tree) { struct s } : t := match s with 
   | Leaf => Leaf
   | Node l y r h =>
       match X.compare x y with
@@ -842,22 +846,22 @@ Fixpoint remove (x:elt)(s:tree) { struct s } : t := match s with
 Lemma remove_avl_1 : forall s x, avl s -> 
  avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1.
 Proof.
- intros s x; functional induction remove x s; simpl; intros.
+ intros s x; functional induction (remove x s); subst;simpl; intros.
  intuition; omega_max.
  (* LT *)
  inv avl.
- destruct (H H1).
+ destruct (IHt H1).
  split. 
  apply bal_avl; auto.
  omega_max.
  omega_bal.
  (* EQ *)
  inv avl. 
- generalize (merge_avl_1 l r H0 H1 H2).
+ generalize (merge_avl_1 l r H1 H2 H3).
  intuition omega_max.
  (* GT *)
  inv avl.
- destruct (H H2).
+ destruct (IHt H2).
  split. 
  apply bal_avl; auto.
  omega_max.
@@ -873,32 +877,32 @@ Hint Resolve remove_avl.
 Lemma remove_in : forall s x y, bst s -> avl s -> 
  (In y (remove x s) <-> ~ X.eq y x /\ In y s).
 Proof.
- intros s x; functional induction remove x s; simpl; intros.
+ intros s x; functional induction (remove x s); subst;simpl; intros.
  intuition_in.
  (* LT *)
- inv avl; inv bst; clear H_eq_0.
+ inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (H y0 H1); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H1); intuition; [ order | order | intuition_in ].
  (* EQ *)
- inv avl; inv bst; clear H_eq_0.
+ inv avl; inv bst; clear H0.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
  elim H9; eauto.
  (* GT *)
- inv avl; inv bst; clear H_eq_0.
+ inv avl; inv bst; clear H0.
  rewrite bal_in; auto.
- generalize (H y0 H6); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H6); intuition; [ order | order | intuition_in ].
 Qed.
 
 Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s).
 Proof. 
- intros s x; functional induction remove x s; simpl; intros.
+ intros s x; functional induction (remove x s); simpl; intros.
  auto.
  (* LT *)
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in l x y0) in H0; auto.
- destruct H0; eauto.
+ rewrite (remove_in l x y0) in H1; auto.
+ destruct H1; eauto.
  (* EQ *)
  inv avl; inv bst.
  apply merge_bst; eauto.
@@ -906,13 +910,13 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in r x y0) in H0; auto.
- destruct H0; eauto.
+ rewrite (remove_in r x y0) in H1; auto.
+ destruct H1; eauto.
 Qed.
 
  (** * Minimum element *)
 
-Fixpoint min_elt (s:t) : option elt := match s with 
+Function min_elt (s:t) : option elt := match s with 
    | Leaf => None
    | Node Leaf y _  _ => Some y
    | Node l _ _ _ => min_elt l
@@ -920,46 +924,48 @@ end.
 
 Lemma min_elt_1 : forall s x, min_elt s = Some x -> In x s. 
 Proof. 
- intro s; functional induction min_elt s; simpl.
+ intro s; functional induction (min_elt s); subst; simpl.
  inversion 1.
  inversion 1; auto.
  intros.
- destruct t0; auto.
+ destruct l; auto.
 Qed.
 
 Lemma min_elt_2 : forall s x y, bst s -> 
  min_elt s = Some x -> In y s -> ~ X.lt y x. 
 Proof.
- intro s; functional induction min_elt s; simpl.
+ intro s; functional induction (min_elt s); subst;simpl.
  inversion_clear 2.
  inversion_clear 1.
  inversion 1; subst.
  inversion_clear 1; auto.
  inversion_clear H5.
+ destruct l;try contradiction.
  inversion_clear 1.
- destruct t0.
+ simpl.
+ destruct l1.
  inversion 1; subst.
- assert (X.lt x y) by (apply H3; auto).
+ assert (X.lt x _x) by (apply H3; auto).
  inversion_clear 1; auto; order.
- assert (X.lt t1 y) by auto.
+ assert (X.lt t _x) by auto.
  inversion_clear 2; auto; 
-   (assert (~ X.lt t1 x) by auto); order.
+   (assert (~ X.lt t x) by auto); order.
 Qed.
 
 Lemma min_elt_3 : forall s, min_elt s = None -> Empty s.
 Proof.
- intro s; functional induction min_elt s; simpl.
+ intro s; functional induction (min_elt s); subst;simpl.
  red; auto.
  inversion 1.
- destruct t0.
- inversion 1.
- intros H0; destruct (H H0 t1); auto.
+ destruct l;try contradiction. 
+ clear H0;intro H0.
+ destruct (IHo H0 t);  auto.
 Qed.
 
 
 (** * Maximum element *)
 
-Fixpoint max_elt (s:t) : option elt := match s with 
+Function max_elt (s:t) : option elt := match s with 
    | Leaf => None
    | Node _ y Leaf  _ => Some y
    | Node _ _ r _ => max_elt r
@@ -967,40 +973,38 @@ end.
 
 Lemma max_elt_1 : forall s x, max_elt s = Some x -> In x s. 
 Proof. 
- intro s; functional induction max_elt s; simpl.
+ intro s; functional induction (max_elt s); subst;simpl.
  inversion 1.
  inversion 1; auto.
- intros.
- destruct t2; auto.
+ destruct r;try contradiction; auto.
 Qed.
 
 Lemma max_elt_2 : forall s x y, bst s -> 
  max_elt s = Some x -> In y s -> ~ X.lt x y. 
 Proof.
- intro s; functional induction max_elt s; simpl.
+ intro s; functional induction (max_elt s); subst;simpl.
  inversion_clear 2.
  inversion_clear 1.
  inversion 1; subst.
  inversion_clear 1; auto.
  inversion_clear H5.
+ destruct r;try contradiction.
  inversion_clear 1.
- destruct t2.
- inversion 1; subst.
- assert (X.lt y x) by (apply H4; auto).
- inversion_clear 1; auto; order.
- assert (X.lt y t1) by auto.
+(*  inversion 1; subst. *)
+(*  assert (X.lt y x) by (apply H4; auto). *)
+(*  inversion_clear 1; auto; order. *)
+ assert (X.lt _x0 t) by auto.
  inversion_clear 2; auto; 
-  (assert (~ X.lt x t1) by auto); order.
+  (assert (~ X.lt x t) by auto); order.
 Qed.
 
 Lemma max_elt_3 : forall s, max_elt s = None -> Empty s.
 Proof.
- intro s; functional induction max_elt s; simpl.
+ intro s; functional induction (max_elt s); subst;simpl.
  red; auto.
  inversion 1.
- destruct t2.
- inversion 1.
- intros H0; destruct (H H0 t1); auto.
+ destruct r;try contradiction.
+ clear H0;intros H0; destruct (IHo H0 t); auto.
 Qed.
 
 (** * Any element *)
@@ -1022,7 +1026,7 @@ Qed.
     Same as [merge] but does not assume anything about heights.
 *)
 
-Definition concat s1 s2 := 
+Function concat (s1 s2 : t) : t  := 
    match s1, s2 with 
       | Leaf, _ => s2 
       | _, Leaf => s1
@@ -1033,46 +1037,39 @@ Definition concat s1 s2 :=
 
 Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
 Proof.
- intros s1 s2; functional induction concat s1 s2; auto.
- intros; change (avl (join (Node t t0 t1 i) m s2')).
- rewrite <- H_eq_ in H; rewrite <- H_eq_.
- apply join_avl; auto.
- generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H_eq_1; simpl; auto.
+ intros s1 s2; functional induction (concat s1 s2); subst;auto.
+ destruct _x;try contradiction;clear H1.
+ intros; apply join_avl; auto.
+ generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H2; simpl; auto.
 Qed.
  
 Lemma concat_bst :   forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (concat s1 s2).
 Proof. 
- intros s1 s2; functional induction concat s1 s2; auto.
- intros; change (bst (join (Node t t0 t1 i) m s2')).
- rewrite <- H_eq_ in H; rewrite <- H_eq_ in H0; 
- rewrite <- H_eq_ in H3; rewrite <- H_eq_.
- apply join_bst; auto.
- generalize (remove_min_bst l2 x2 r2 h2 H1 H2); rewrite H_eq_1; simpl; auto.
- generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite H_eq_1; simpl; auto.
- generalize (remove_min_in l2 x2 r2 h2 m H2); rewrite H_eq_1; simpl; auto.
+ intros s1 s2; functional induction (concat s1 s2); subst ;auto.
+ destruct _x;try contradiction;clear H1. 
+ intros;  apply join_bst; auto.
+ generalize (remove_min_bst l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto.
+ generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
+ generalize (remove_min_in l2 x2 r2 h2 m H3); rewrite H2; simpl; auto.
  destruct 1; intuition.
- generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H2); rewrite H_eq_1; simpl; auto.
+ generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto.
 Qed.
 
 Lemma concat_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
  (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  (In y (concat s1 s2) <-> In y s1 \/ In y s2).
 Proof.
- intros s1 s2; functional induction concat s1 s2.
+ intros s1 s2; functional induction (concat s1 s2);subst;simpl.
  intuition.
  inversion_clear H5.
- intuition.
+ destruct _x;try contradiction;clear H1;intuition.
  inversion_clear H5.
- intros. 
- change (In y (join (Node t t0 t1 i) m s2') <-> 
-              In y (Node t t0 t1 i) \/ In y (Node l2 x2 r2 h2)).
- rewrite <- H_eq_ in H; rewrite <- H_eq_ in H0; 
- rewrite <- H_eq_ in H3; rewrite <- H_eq_.
- rewrite (join_in s1 m s2' y H0).
- generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite H_eq_1; simpl; auto.
- generalize (remove_min_in l2 x2 r2 h2 y H2); rewrite H_eq_1; simpl.
+ destruct _x;try contradiction;clear H1; intros. 
+ rewrite (join_in  (Node _x1 t _x2 i) m s2' y H0).
+ generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
+ generalize (remove_min_in l2 x2 r2 h2 y H3); rewrite H2; simpl.
  intro EQ; rewrite EQ; intuition.
 Qed.
 
@@ -1084,7 +1081,7 @@ Qed.
     - [present] is [true] if and only if [s] contains  [x].
 *)
 
-Fixpoint split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with 
+Function split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with 
   | Leaf => (Leaf, (false, Leaf))
   | Node l y r h => 
      match X.compare x y with 
@@ -1101,101 +1098,99 @@ Fixpoint split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with
 Lemma split_avl : forall s x, avl s -> 
   avl (fst (split x s)) /\ avl (snd (snd (split x s))).
 Proof. 
- intros s x; functional induction split x s.
+ intros s x; functional induction (split x s);subst;simpl in *.
  auto.
- destruct p; simpl in *.
- inversion_clear 1; intuition.
+ rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition.
  simpl; inversion_clear 1; auto.
- destruct p; simpl in *.
- inversion_clear 1; intuition.
+ rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition.
 Qed.
 
 Lemma split_in_1 : forall s x y, bst s -> avl s -> 
  (In y (fst (split x s)) <-> In y s /\ X.lt y x).
 Proof. 
- intros s x; functional induction split x s.
+ intros s x; functional induction (split x s);subst;simpl in *.
  intuition; try inversion_clear H1.
  (* LT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8.
- rewrite (H y0 H1 H5); clear H H_eq_0.
+ rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear  H8 H9.
+ rewrite (IHp y0 H2 H6); clear IHp H0.
  intuition.
  inversion_clear H0; auto; order.
  (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H7 H_eq_0.
+ simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0.
  intuition.
  order.
  intuition_in; order.
  (* GT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8.
+ rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
  rewrite join_in; auto.
- generalize (split_avl r x H6); rewrite H_eq_1; simpl; intuition.
- rewrite (H y0 H2 H6); clear H.
+ generalize (split_avl r x H7); rewrite H1; simpl; intuition.
+ rewrite (IHp y0 H3 H7); clear H1.
  intuition; [ eauto | eauto | intuition_in ].
 Qed.
 
 Lemma split_in_2 : forall s x y, bst s -> avl s -> 
  (In y (snd (snd (split x s))) <-> In y s /\ X.lt x y).
 Proof. 
- intros s x; functional induction split x s.
+ intros s x; functional induction (split x s);subst;simpl in *.
  intuition; try inversion_clear H1.
  (* LT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8.
+ rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
   rewrite join_in; auto.
- generalize (split_avl l x H5); rewrite H_eq_1; simpl; intuition.
- rewrite (H y0 H1 H5); clear H H_eq_0.
+ generalize (split_avl l x H6); rewrite H1; simpl; intuition.
+ rewrite (IHp y0 H2 H6); clear IHp H0.
  intuition; [ order | order | intuition_in ].
  (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H7 H_eq_0.
+ simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0.
  intuition; [ order | intuition_in; order ]. 
  (* GT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8.
- rewrite (H y0 H2 H6); clear H H_eq_0.
+ rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
+ rewrite (IHp y0 H3 H7); clear IHp H0.
  intuition; intuition_in; order. 
 Qed.
 
 Lemma split_in_3 : forall s x, bst s -> avl s -> 
  (fst (snd (split x s)) = true <-> In x s).
 Proof. 
- intros s x; functional induction split x s.
+ intros s x; functional induction (split x s);subst;simpl in *.
  intuition; try inversion_clear H1.
  (* LT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8.
- rewrite H; auto.
+ rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
+ rewrite IHp; auto.
  intuition_in; absurd (X.lt x y); eauto.
  (* EQ *)
  simpl in *; inversion_clear 1; inversion_clear 1; intuition.
  (* GT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8.
- rewrite H; auto.
+ rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
+ rewrite IHp; auto.
  intuition_in; absurd (X.lt y x); eauto.
 Qed.
 
 Lemma split_bst : forall s x, bst s -> avl s -> 
  bst (fst (split x s)) /\ bst (snd (snd (split x s))).
 Proof. 
- intros s x; functional induction split x s.
+ intros s x; functional induction (split x s);subst;simpl in *.  
  intuition.
  (* LT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1.
+ rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
  intuition.
  apply join_bst; auto.
- generalize (split_avl l x H5); rewrite H_eq_1; simpl; intuition.
+ generalize (split_avl l x H6); rewrite H1; simpl; intuition.
  intro; intro.
- generalize (split_in_2 l x y0 H1 H5); rewrite H_eq_1; simpl; intuition.
+ generalize (split_in_2 l x y0 H2 H6); rewrite H1; simpl; intuition.
  (* EQ *)
  simpl in *; inversion_clear 1; inversion_clear 1; intuition.
  (* GT *)
- destruct p; simpl in *; inversion_clear 1; inversion_clear 1.
+ rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
  intuition.
  apply join_bst; auto.
- generalize (split_avl r x H6); rewrite H_eq_1; simpl; intuition.
+ generalize (split_avl r x H7); rewrite H1; simpl; intuition.
  intro; intro.
- generalize (split_in_1 r x y0 H2 H6); rewrite H_eq_1; simpl; intuition.
+ generalize (split_in_1 r x y0 H3 H7); rewrite H1; simpl; intuition.
 Qed.
 
 (** * Intersection *)
 
- Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with 
+Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with 
     | Leaf,_ => Leaf
     | _,Leaf => Leaf
     | Node l1 x1 r1 h1, _ =>