--- a/src/GeneralRec.v	Sat Aug 19 12:14:26 2017 -0400
+++ b/src/GeneralRec.v	Sat Aug 19 12:14:40 2017 -0400
@@ -822,10 +822,7 @@
   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.
+  try subst B. (* This line expected to fail in Coq 8.4 and succeed in Coq 8.6. *)
   crush.
   inversion H; clear H; crush.
   eauto.
@@ -839,10 +836,7 @@
   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.
+  try subst A. (* Same as above *)
   crush.
   inversion H0; clear H0; crush.
   eauto.