Merge PR #13730: Lint stdlib with -mangle-names #6

Reviewed-by: anton-trunov

1 files changed, 123 insertions, 102 deletions

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 826815410a..69b158a87e 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -71,7 +71,7 @@ Hint Constructors NoDupA : core.
 Lemma NoDupA_altdef : forall l,
  NoDupA l <-> ForallOrdPairs (complement eqA) l.
 Proof.
- split; induction 1; constructor; auto.
+ split; induction 1 as [|a l H rest]; constructor; auto.
  rewrite Forall_forall. intros b Hb.
  intro Eq; elim H. rewrite InA_alt. exists b; auto.
  rewrite InA_alt; intros (a' & Haa' & Ha').
@@ -85,7 +85,7 @@ Definition inclA l l' := forall x, InA x l -> InA x l'.
 Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
 
 Lemma incl_nil l : inclA nil l.
-Proof. intro. intros. inversion H. Qed.
+Proof. intros a H. inversion H. Qed.
 #[local]
 Hint Resolve incl_nil : list.
 
@@ -128,7 +128,7 @@ Qed.
 Global Instance eqlistA_equiv : Equivalence eqlistA.
 Proof.
  constructor; red.
- induction x; auto.
+ intros x; induction x; auto.
  induction 1; auto.
  intros x y z H; revert z; induction H; auto.
  inversion 1; subst; auto. invlist eqlistA; eauto with *.
@@ -138,9 +138,9 @@ Qed.
 
 Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA.
 Proof.
-  intros x x' H. induction H.
+  intros x x' H. induction H as [|? ? ? ? H ? IHeqlistA].
   intuition.
-  red; intros.
+  red; intros x0.
   rewrite 2 InA_cons.
   rewrite (IHeqlistA x0), H; intuition.
 Qed.
@@ -165,7 +165,7 @@ Hint Immediate InA_eqA : core.
 
 Lemma In_InA : forall l x, In x l -> InA x l.
 Proof.
- simple induction l; simpl; intuition.
+ intros l; induction l; simpl; intuition.
  subst; auto.
 Qed.
 #[local]
@@ -174,8 +174,9 @@ Hint Resolve In_InA : core.
 Lemma InA_split : forall l x, InA x l ->
  exists l1 y l2, eqA x y /\ l = l1++y::l2.
 Proof.
-induction l; intros; inv.
+intros l; induction l as [|a l IHl]; intros x H; inv.
 exists (@nil A); exists a; exists l; auto.
+match goal with H' : InA x l |- _ => rename H' into H0 end.
 destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))).
 exists (a::l1); exists y; exists l2; auto.
 split; simpl; f_equal; auto.
@@ -184,9 +185,10 @@ Qed.
 Lemma InA_app : forall l1 l2 x,
  InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
 Proof.
- induction l1; simpl in *; intuition.
+ intros l1; induction l1 as [|a l1 IHl1]; simpl in *; intuition.
  inv; auto.
- elim (IHl1 l2 x H0); auto.
+ match goal with H0' : InA _ (l1 ++ _) |- _ => rename H0' into H0 end.
+ elim (IHl1 _ _ H0); auto.
 Qed.
 
 Lemma InA_app_iff : forall l1 l2 x,
@@ -194,7 +196,7 @@ Lemma InA_app_iff : forall l1 l2 x,
 Proof.
  split.
  apply InA_app.
- destruct 1; generalize H; do 2 rewrite InA_alt.
+ destruct 1 as [H|H]; generalize H; do 2 rewrite InA_alt.
  destruct 1 as (y,(H1,H2)); exists y; split; auto.
  apply in_or_app; auto.
  destruct 1 as (y,(H1,H2)); exists y; split; auto.
@@ -240,11 +242,12 @@ Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->
   (forall x, InA x l -> InA x l' -> False) ->
   NoDupA (l++l').
 Proof.
-induction l; simpl; auto; intros.
+intros l; induction l as [|a l IHl]; simpl; auto; intros l' H H0 H1.
 inv.
 constructor.
 rewrite InA_alt; intros (y,(H4,H5)).
 destruct (in_app_or _ _ _ H5).
+match goal with H2' : ~ InA a l |- _ => rename H2' into H2 end.
 elim H2.
 rewrite InA_alt.
 exists y; auto.
@@ -253,13 +256,13 @@ auto.
 rewrite InA_alt.
 exists y; auto.
 apply IHl; auto.
-intros.
+intros x ? ?.
 apply (H1 x); auto.
 Qed.
 
 Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
 Proof.
-induction l.
+intros l; induction l.
 simpl; auto.
 simpl; intros.
 inv.
@@ -270,17 +273,17 @@ intros x.
 rewrite InA_alt.
 intros (x1,(H2,H3)).
 intro; inv.
-destruct H0.
-rewrite <- H4, H2.
+match goal with H0 : ~ InA _ _ |- _ => destruct H0 end.
+match goal with H4 : eqA x ?x' |- InA ?x' _ => rewrite <- H4, H2 end.
 apply In_InA.
 rewrite In_rev; auto.
 Qed.
 
 Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
 Proof.
- induction l; simpl in *; intros; inv; auto.
+ intros l; induction l; simpl in *; intros; inv; auto.
  constructor; eauto.
- contradict H0.
+ match goal with H0 : ~ InA _ _ |- _ => contradict H0 end.
  rewrite InA_app_iff in *.
  rewrite InA_cons.
  intuition.
@@ -288,17 +291,17 @@ Qed.
 
 Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
 Proof.
- induction l; simpl in *; intros; inv; auto.
+ intros l; induction l as [|a l IHl]; simpl in *; intros l' x H; inv; auto.
  constructor; eauto.
- assert (H2:=IHl _ _ H1).
+ match goal with H1 : NoDupA (l ++ x :: l') |- _ => assert (H2:=IHl _ _ H1) end.
  inv.
  rewrite InA_cons.
  red; destruct 1.
- apply H0.
+ match goal with H0 : ~ InA a (l ++ x :: l') |- _ => apply H0 end.
  rewrite InA_app_iff in *; rewrite InA_cons; auto.
- apply H; auto.
+ auto.
  constructor.
- contradict H0.
+ match goal with H0 : ~ InA a (l ++ x :: l') |- _ => contradict H0 end.
  rewrite InA_app_iff in *; rewrite InA_cons; intuition.
  eapply NoDupA_split; eauto.
 Qed.
@@ -356,19 +359,21 @@ Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y ->
  NoDupA (x::l) -> NoDupA (l1++y::l2) ->
  equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
 Proof.
- intros; intro a.
+ intros H H0 H1 H2; intro a.
  generalize (H2 a).
  rewrite !InA_app_iff, !InA_cons.
  inv.
  assert (SW:=NoDupA_swap H1). inv.
- rewrite InA_app_iff in H0.
+ rewrite InA_app_iff in *.
  split; intros.
- assert (~eqA a x) by (contradict H3; rewrite <- H3; auto).
+ match goal with H3 : ~ InA x l |- _ =>
+   assert (~eqA a x) by (contradict H3; rewrite <- H3; auto)
+ end.
  assert (~eqA a y) by (rewrite <- H; auto).
  tauto.
- assert (OR : eqA a x \/ InA a l) by intuition. clear H6.
+ assert (OR : eqA a x \/ InA a l) by intuition.
  destruct OR as [EQN|INA]; auto.
- elim H0.
+ match goal with H0 : ~ (InA y l1 \/ InA y l2) |- _ => elim H0 end.
  rewrite <-H,<-EQN; auto.
 Qed.
 
@@ -448,7 +453,7 @@ Qed.
 Lemma ForallOrdPairs_inclA : forall l l',
  NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'.
 Proof.
-induction l' as [|x l' IH].
+intros l l'. induction l' as [|x l' IH].
 constructor.
 intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto.
 rewrite Forall_forall; intros y Hy.
@@ -476,7 +481,7 @@ Lemma fold_right_commutes_restr :
   forall s1 s2 x, ForallOrdPairs R (s1++x::s2) ->
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
-induction s1; simpl; auto; intros.
+intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x H.
 reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))).
 apply Comp; auto.
@@ -484,7 +489,9 @@ apply IHs1.
 invlist ForallOrdPairs; auto.
 apply TraR.
 invlist ForallOrdPairs; auto.
-rewrite Forall_forall in H0; apply H0.
+match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- R a x =>
+  rewrite Forall_forall in H0; apply H0
+end.
 apply in_or_app; simpl; auto.
 Qed.
 
@@ -492,14 +499,14 @@ Lemma fold_right_equivlistA_restr :
   forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
- simple induction s.
- destruct s'; simpl.
+ intros s; induction s as [|x l Hrec].
+ intros s'; destruct s' as [|a s']; simpl.
  intros; reflexivity.
- unfold equivlistA; intros.
+ unfold equivlistA; intros H H0 H1 H2.
  destruct (H2 a).
  assert (InA a nil) by auto; inv.
- intros x l Hrec s' N N' F E; simpl in *.
- assert (InA x s') by (rewrite <- (E x); auto).
+ intros s' N N' F E; simpl in *.
+ assert (InA x s') as H by (rewrite <- (E x); auto).
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
  transitivity (f x (fold_right f i (s1++s2))).
@@ -520,7 +527,7 @@ Lemma fold_right_add_restr :
   forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
 Proof.
- intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
+ intros s' s x **; apply (@fold_right_equivlistA_restr s' (x::s)); auto.
 Qed.
 
 End Fold_With_Restriction.
@@ -532,7 +539,7 @@ Variable Tra :transpose f.
 Lemma fold_right_commutes : forall s1 s2 x,
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
-induction s1; simpl; auto; intros.
+intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x.
 reflexivity.
 transitivity (f a (f x (fold_right f i (s1++s2)))); auto.
 apply Comp; auto.
@@ -542,7 +549,7 @@ Lemma fold_right_equivlistA :
   forall s s', NoDupA s -> NoDupA s' ->
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
 Proof.
-intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True);
+intros; apply (fold_right_equivlistA_restr (R:=fun _ _ => True));
  repeat red; auto.
 apply ForallPairs_ForallOrdPairs; try red; auto.
 Qed.
@@ -551,7 +558,7 @@ Lemma fold_right_add :
   forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
 Proof.
- intros; apply (@fold_right_equivlistA s' (x::s)); auto.
+ intros s' s x **; apply (@fold_right_equivlistA s' (x::s)); auto.
 Qed.
 
 End Fold.
@@ -571,7 +578,7 @@ Lemma fold_right_eqlistA2 :
   eqB (fold_right f i s) (fold_right f j s').
 Proof.
   intros s.
-  induction s;intros.
+  induction s as [|a s IHs];intros s' i j heqij heqss'.
   - inversion heqss'.
     subst.
     simpl.
@@ -604,7 +611,7 @@ Lemma fold_right_commutes_restr2 :
   forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) ->
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))).
 Proof.
-induction s1; simpl; auto; intros.
+intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x i j heqij ?.
 - apply Comp.
   + destruct eqA_equiv. apply Equivalence_Reflexive.
   + eapply fold_right_eqlistA2.
@@ -617,7 +624,9 @@ induction s1; simpl; auto; intros.
   invlist ForallOrdPairs; auto.
   apply TraR.
   invlist ForallOrdPairs; auto.
-  rewrite Forall_forall in H0; apply H0.
+  match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- _ =>
+    rewrite Forall_forall in H0; apply H0
+  end.
   apply in_or_app; simpl; auto.
   reflexivity.
 Qed.
@@ -628,14 +637,14 @@ Lemma fold_right_equivlistA_restr2 :
     equivlistA s s' -> eqB i j ->
     eqB (fold_right f i s) (fold_right f j s').
 Proof.
- simple induction s.
- destruct s'; simpl.
+ intros s; induction s as [|x l Hrec].
+ intros s'; destruct s' as [|a s']; simpl.
  intros. assumption.
- unfold equivlistA; intros.
+ unfold equivlistA; intros ? ? H H0 H1 H2 **.
  destruct (H2 a).
  assert (InA a nil) by auto; inv.
- intros x l Hrec s' i j N N' F E eqij; simpl in *.
- assert (InA x s') by (rewrite <- (E x); auto).
+ intros s' i j N N' F E eqij; simpl in *.
+ assert (InA x s') as H by (rewrite <- (E x); auto).
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
  transitivity (f x (fold_right f j (s1++s2))).
@@ -663,7 +672,7 @@ Lemma fold_right_add_restr2 :
   forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
 Proof.
- intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto.
+ intros s' s i j x **; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto.
 Qed.
 
 End Fold2_With_Restriction.
@@ -674,7 +683,7 @@ Lemma fold_right_commutes2 : forall s1 s2 i x x',
   eqA x x' -> 
   eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))).
 Proof.
-  induction s1;simpl;intros.
+  intros s1; induction s1 as [|a s1 IHs1];simpl;intros s2 i x x' H.
 - apply Comp;auto.
   reflexivity.
 - transitivity (f a (f x' (fold_right f i (s1++s2)))); auto.
@@ -688,7 +697,7 @@ Lemma fold_right_equivlistA2 :
   equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
 Proof.
 red in Tra.
-intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True);
+intros; apply (fold_right_equivlistA_restr2 (R:=fun _ _ => True));
 repeat red; auto.
 apply ForallPairs_ForallOrdPairs; try red; auto.
 Qed.
@@ -697,9 +706,9 @@ Lemma fold_right_add2 :
   forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
 Proof.
- intros.
+ intros s' s i j x **.
  replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto.
- eapply fold_right_equivlistA2;auto. 
+ eapply fold_right_equivlistA2;auto.
 Qed.
 
 End Fold2.
@@ -710,7 +719,7 @@ Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
 Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
 Proof.
-induction l.
+intros x l; induction l as [|a l IHl].
 right; auto.
 intro; inv.
 destruct (eqA_dec x a).
@@ -729,28 +738,30 @@ Fixpoint removeA (x : A) (l : list A) : list A :=
 Lemma removeA_filter : forall x l,
   removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
 Proof.
-induction l; simpl; auto.
+intros x l; induction l as [|a l IHl]; simpl; auto.
 destruct (eqA_dec x a); auto.
 rewrite IHl; auto.
 Qed.
 
 Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
 Proof.
-induction l; simpl; auto.
-split.
+intros l; induction l as [|a l IHl]; simpl; auto.
+intros x y; split.
 intro; inv.
 destruct 1; inv.
-intros.
+intros x y.
 destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto.
 rewrite IHl; split; destruct 1; split; auto.
 inv; auto.
-destruct H0; transitivity a; auto.
+match goal with H0 : ~ eqA x y |- _ => destruct H0 end; transitivity a; auto.
 split.
 intro; inv.
 split; auto.
 contradict Hnot.
 transitivity y; auto.
-rewrite (IHl x y) in H0; destruct H0; auto.
+match goal with H0 : InA y (removeA x l) |- _ =>
+  rewrite (IHl x y) in H0; destruct H0; auto
+end.
 destruct 1; inv; auto.
 right; rewrite IHl; auto.
 Qed.
@@ -758,7 +769,7 @@ Qed.
 Lemma removeA_NoDupA :
   forall s x, NoDupA s ->  NoDupA (removeA x s).
 Proof.
-simple induction s; simpl; intros.
+intros s; induction s as [|a s IHs]; simpl; intros x ?.
 auto.
 inv.
 destruct (eqA_dec x a); simpl; auto.
@@ -770,16 +781,16 @@ Qed.
 Lemma removeA_equivlistA : forall l l' x,
   ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
 Proof.
-unfold equivlistA; intros.
+unfold equivlistA; intros l l' x H H0 x0.
 rewrite removeA_InA.
-split; intros.
+split; intros H1.
 rewrite <- H0; split; auto.
 contradict H.
 apply InA_eqA with x0; auto.
 rewrite <- (H0 x0) in H1.
 destruct H1.
 inv; auto.
-elim H2; auto.
+match goal with H2 : ~ eqA x x0 |- _ => elim H2; auto end.
 Qed.
 
 End Remove.
@@ -806,7 +817,7 @@ Hint Constructors lelistA sort : core.
 Lemma InfA_ltA :
  forall l x y, ltA x y -> InfA y l -> InfA x l.
 Proof.
- destruct l; constructor. inv; eauto.
+ intros l; destruct l; constructor. inv; eauto.
 Qed.
 
 Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
@@ -815,8 +826,8 @@ Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *)
  inversion_clear Hll'.
  intuition.
  split; intro; inv; constructor.
- rewrite <- Hxx', <- H; auto.
- rewrite Hxx', H; auto.
+ match goal with H : eqA _ _ |- _ => rewrite <- Hxx', <- H; auto end.
+ match goal with H : eqA _ _ |- _ => rewrite Hxx', H; auto end.
 Qed.
 
 (** For compatibility, can be deduced from [InfA_compat] *)
@@ -830,9 +841,9 @@ Hint Immediate InfA_ltA InfA_eqA : core.
 Lemma SortA_InfA_InA :
  forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
 Proof.
- simple induction l.
- intros. inv.
- intros. inv.
+ intros l; induction l as [|a l IHl].
+ intros x a **. inv.
+ intros x a0 **. inv.
  setoid_replace x with a; auto.
  eauto.
 Qed.
@@ -840,13 +851,13 @@ Qed.
 Lemma In_InfA :
  forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
 Proof.
- simple induction l; simpl; intros; constructor; auto.
+ intros l; induction l; simpl; intros; constructor; auto.
 Qed.
 
 Lemma InA_InfA :
  forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
 Proof.
- simple induction l; simpl; intros; constructor; auto.
+ intros l; induction l; simpl; intros; constructor; auto.
 Qed.
 
 (* In fact, this may be used as an alternative definition for InfA: *)
@@ -861,7 +872,7 @@ Qed.
 
 Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
 Proof.
- induction l1; simpl; auto.
+ intros l1; induction l1; simpl; auto.
  intros; inv; auto.
 Qed.
 
@@ -870,7 +881,7 @@ Lemma SortA_app :
  (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
  SortA (l1 ++ l2).
 Proof.
- induction l1; simpl in *; intuition.
+ intros l1; induction l1; intros l2; simpl in *; intuition.
  inv.
  constructor; auto.
  apply InfA_app; auto.
@@ -879,8 +890,8 @@ Qed.
 
 Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
 Proof.
- simple induction l; auto.
- intros x l' H H0.
+ intros l; induction l as [|x l' H]; auto.
+ intros H0.
  inv.
  constructor; auto.
  intro.
@@ -922,7 +933,7 @@ Qed.
 
 Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
 Proof.
-repeat red. intros.
+repeat red. intros x y ?.
 rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)).
 apply eqlistA_rev_app; auto.
 Qed.
@@ -936,15 +947,15 @@ Qed.
 Lemma SortA_equivlistA_eqlistA : forall l l',
    SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
 Proof.
-induction l; destruct l'; simpl; intros; auto.
-destruct (H1 a); assert (InA a nil) by auto; inv.
+intros l; induction l as [|a l IHl]; intros l'; destruct l' as [|a0 l']; simpl; intros H H0 H1; auto.
+destruct (H1 a0); assert (InA a0 nil) by auto; inv.
 destruct (H1 a); assert (InA a nil) by auto; inv.
 inv.
 assert (forall y, InA y l -> ltA a y).
-intros; eapply SortA_InfA_InA with (l:=l); eauto.
+intros; eapply (SortA_InfA_InA (l:=l)); eauto.
 assert (forall y, InA y l' -> ltA a0 y).
-intros; eapply SortA_InfA_InA with (l:=l'); eauto.
-clear H3 H4.
+intros; eapply (SortA_InfA_InA (l:=l')); eauto.
+do 2 match goal with H : InfA _ _ |- _ => clear H end.
 assert (eqA a a0).
  destruct (H1 a).
  destruct (H1 a0).
@@ -953,13 +964,19 @@ assert (eqA a a0).
  elim (StrictOrder_Irreflexive a); eauto.
 constructor; auto.
 apply IHl; auto.
-split; intros.
+intros x; split; intros.
 destruct (H1 x).
 assert (InA x (a0::l')) by auto. inv; auto.
-rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto.
+match goal with H3 : eqA a a0, H4 : InA x l, H9 : eqA x a0 |- InA x l' =>
+  rewrite H9,<-H3 in H4
+end.
+elim (StrictOrder_Irreflexive a); eauto.
 destruct (H1 x).
 assert (InA x (a::l)) by auto. inv; auto.
-rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto.
+match goal with H3 : eqA a a0, H4 : InA x l', H9 : eqA x a |- InA x l =>
+  rewrite H9,H3 in H4
+end.
+elim (StrictOrder_Irreflexive a0); eauto.
 Qed.
 
 End EqlistA.
@@ -970,12 +987,12 @@ Section Filter.
 
 Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
 Proof.
-induction l; simpl; auto.
+intros f l; induction l as [|a l IHl]; simpl; auto.
 intros; inv; auto.
 destruct (f a); auto.
 constructor; auto.
 apply In_InfA; auto.
-intros.
+intros y H.
 rewrite filter_In in H; destruct H.
 eapply SortA_InfA_InA; eauto.
 Qed.
@@ -984,12 +1001,14 @@ Arguments eq {A} x _.
 Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
  forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
 Proof.
+(* Unset Mangle Names. *)
 clear sotrans ltA ltA_strorder ltA_compat.
-intros; do 2 rewrite InA_alt; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
-destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
+intros f H l x; do 2 rewrite InA_alt; intuition;
+  match goal with Hex' : exists _, _ |- _ => rename Hex' into Hex end.
+destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
+destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; intuition.
   rewrite (H _ _ H0); auto.
-destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
+destruct Hex as (y,(H0,H1)); exists y; rewrite filter_In; intuition.
   rewrite <- (H _ _ H0); auto.
 Qed.
 
@@ -997,19 +1016,20 @@ Lemma filter_split :
  forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
  forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
 Proof.
-induction l; simpl; intros; auto.
+intros f H l; induction l as [|a l IHl]; simpl; intros H0; auto.
 inv.
+match goal with H1' : SortA l, H2' : InfA a l |- _ => rename H1' into H1, H2' into H2 end.
 rewrite IHl at 1; auto.
 case_eq (f a); simpl; intros; auto.
-assert (forall e, In e l -> f e = false).
-  intros.
+assert (forall e, In e l -> f e = false) as H3.
+  intros e H3.
   assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)).
   case_eq (f e); simpl; intros; auto.
   elim (StrictOrder_Irreflexive e).
   transitivity a; auto.
 replace (List.filter f l) with (@nil A); auto.
-generalize H3; clear; induction l; simpl; auto.
-case_eq (f a); auto; intros.
+generalize H3; clear; induction l as [|a l IHl]; simpl; auto.
+case_eq (f a); auto; intros H H3.
 rewrite H3 in H; auto; try discriminate.
 Qed.
 
@@ -1043,23 +1063,24 @@ Lemma findA_NoDupA :
 Proof.
 set (eqk := fun p p' : A*B => eqA (fst p) (fst p')).
 set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p').
-induction l; intros; simpl.
-split; intros; try discriminate.
+intros l; induction l as [|a l IHl]; intros a0 b H; simpl.
+split; intros H0; try discriminate.
 invlist InA.
 destruct a as (a',b'); rename a0 into a.
 invlist NoDupA.
 split; intros.
 invlist InA.
-compute in H2; destruct H2. subst b'.
+match goal with H2 : eqke (a, b) (a', b') |- _ => compute in H2; destruct H2 end.
+subst b'.
 destruct (eqA_dec a a'); intuition.
 destruct (eqA_dec a a') as [HeqA|]; simpl.
-contradict H0.
-revert HeqA H2; clear - eqA_equiv.
+match goal with H0 : ~ InA eqk (a', b') l |- _ => contradict H0 end.
+match goal with H2 : InA eqke (a, b) l |- _ => revert HeqA H2; clear - eqA_equiv end.
 induction l.
 intros; invlist InA.
 intros; invlist InA; auto.
-destruct a0.
-compute in H; destruct H.
+match goal with |- InA eqk _ (?p :: _) => destruct p as [a0 b0] end.
+match goal with H : eqke (a, b) (a0, b0) |- _ => compute in H; destruct H end.
 subst b.
 left; auto.
 compute.