@@ -237,7 +237,6 @@ which is trivially provable using reflexivity:
237 Proof completed!
237 Proof completed!
238 Main.plusredZ_S = %runElab (do intro `{{k}}
238 Main.plusredZ_S = %runElab (do intro `{{k}}
239 intro `{{ih}}
239 intro `{{ih}}
241 rewriteWith (Var `{{ih}})
240 rewriteWith (Var `{{ih}})
242 reflexivity)
241 reflexivity)