--- a/src/GeneralRec.v	Thu May 12 18:09:36 2016 -0500
+++ b/src/GeneralRec.v	Wed Jul 12 13:08:24 2017 -0400
@@ -822,10 +822,6 @@
   match goal with
     | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
   end.
-  move H3 after A.
-  generalize dependent B0.
-  do 2 intro.
-  subst.
   crush.
   inversion H; clear H; crush.
   eauto.
@@ -839,10 +835,6 @@
   match goal with
     | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
   end.
-  move H3 after B.
-  generalize dependent B0.
-  do 2 intro.
-  subst.
   crush.
   inversion H0; clear H0; crush.
   eauto.