--- a/src/GeneralRec.v	Wed Jul 12 13:33:23 2017 -0400
+++ b/src/GeneralRec.v	Wed Jul 12 13:49:46 2017 -0400
@@ -822,7 +822,7 @@
   match goal with
     | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
   end.
-  subst B.
+  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.
@@ -836,7 +836,7 @@
   match goal with
     | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
   end.
-  subst A.
+  try subst A. (* Same as above *)
   crush.
   inversion H0; clear H0; crush.
   eauto.