hunk ./Basics.v 300
-  Next Obligation. simpl_morph. Qed.
+  Next Obligation. intros a a' Aa b b' Bb. unfold const. auto. Qed.
hunk ./Basics.v 329
-Program Instance option_eq_trans : Transitive (@option_eq A) :=
-(fun x y z Hxy Hyz 
-  => match Hxy, Hyz with
-       | option_eq_Some x' y'0 Hxy', option_eq_Some y'1 z' Hyz'
-         => @option_eq_Some A x' y'0 (transitivity Hxy' Hyz')
-       | option_eq_None, option_eq_None => option_eq_None
-       | option_eq_Some x' y' Hxy', option_eq_None => _
-       | option_eq_None, option_eq_Some y' z' Hyz' => _
-     end).
-Next Obligation.
-  pose (Heq_y' := JMeq_eq (y:=y) Heq_y).
-  clear Heq_Hxy.
-  intro.
-  dependent destruction Heq_y.
-Program Definition option_setoid (A : Setoid) : Setoid :=
-  {| car := option A ; seq := option_eq |}.
hunk ./Basics.v 330
-  Next Obligation.
-    constructor ; red ; intros.
+Program Instance option_eq_trans : Transitive (@option_eq A).
hunk ./Basics.v 332
-    destruct x ; simpl; constructor; reflexivity.
-    destruct H. rewrite H.
-    destruct x ; destruct y ; simpl ; auto with relations.
-    simpl in H. now symmetry.
-    destruct x ; destruct y ; destruct z ; simpl in * ; auto with relations.
-    now transitivity c0.
-    inversion H.
+  Next Obligation.
+    induction H; depelim H0. constructor. now transitivity y.
+    constructor.
hunk ./Basics.v 337
+Program Definition option_setoid (A : Setoid) : Setoid :=
+  {| car := option A ; seq := option_eq |}.
+
+  Next Obligation. constructor; typeclasses eauto. Qed.
+
hunk ./Laws.v 10
+
+Global Generalizable All Variables.
hunk ./List.v 31
-Instance eqlistA_equiv `{E : Equivalence α eqα} : Equivalence (eqlistA eqα).
-Proof.
-  intros ; constructor ; red.
-
-  induction x ; eauto. constructor ; auto. reflexivity.
-
-  induction 1 ; [eauto | constructor ; auto ; now symmetry ].
-
-  intros x y z H ; revert z ; induction H ; intros ; [eauto | try constructor ; auto].
-  inversion H1 ; subst. constructor. transitivity x' ; auto.
-  apply IHeqlistA. auto.
-Qed.
+Print Hint Equivalence.
hunk ./List.v 66
-  Proof. now rewrite map_id. Qed.
-
+  Proof. rewrite map_compose. reflexivity. Qed.
+    
hunk ./List.v 69
-  Proof. 
-    rewrite map_compose. reflexivity.
-  Qed.
+  Proof. now rewrite map_id. Qed.
hunk ./List.v 95
-Equations_nocomp concat {A} (l : list (list A)) : list A :=
+Require Import Equations.
+
+Equations(nocomp) concat {A} (l : list (list A)) : list A :=
hunk ./List.v 99
-concat A (x :: xs) := x ++ concat xs.
+concat A (cons x xs) := x ++ concat xs.
hunk ./List.v 110
-  intros. do 2 red. induction 1; simpl ; auto.
+  intros. do 2 red. induction 1; simp concat ; auto.
hunk ./List.v 117
-  Next Obligation. simpl in *. rewrite H. reflexivity. Qed.
+  Next Obligation. simpl in *. now rewrite H. Qed.
hunk ./List.v 122
-  induction l ; simpl ; intros ; auto.
-  reflexivity.
+  induction l ; simpl; intros; simp concat ; auto.
+  reflexivity.   unfold Equivalence.equiv in *.
hunk ./Num.v 197
-  Next Obligation. assert(H:=do_subrelation). typeclasses eauto. Qed.
hunk ./Num.v 202
-  Next Obligation. assert(H:=do_subrelation). typeclasses eauto. Qed.
hunk ./Num.v 209
-Tactic Notation "ring" "*" := autosimpl ; ring.
+Tactic Notation "ring" "*" := autounfold with typeclass_instances; ring.