diff --git a/lib/ppast.ml b/lib/ppast.ml
index 8b1fbce8..12c90363 100644
--- a/lib/ppast.ml
+++ b/lib/ppast.ml
@@ -306,7 +306,9 @@ let pp_induction_clause printer = function
       in
       pp_destruction_arg printer arg;
       pp_as_list as_list
-  | _, (Some _, _), None -> write printer "n eqn:E"
+  | arg, (Some _, _), None ->
+      pp_destruction_arg printer arg;
+      write printer " eqn:E"
   | _ -> raise (NotImplemented (contents printer))
 
 let pp_induction_clause_list printer = function