From c092788296843c7511cee7a510ca734852be2d09 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 8 Dec 2023 11:49:32 +0900 Subject: [PATCH] remove unnecessary parentheses --- lib/ssr_ext.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ssr_ext.v b/lib/ssr_ext.v index a1af1396..10d72b64 100644 --- a/lib/ssr_ext.v +++ b/lib/ssr_ext.v @@ -704,7 +704,7 @@ Proof. subst m n => /=. case => /= tv. apply eq_from_tnth => i. -rewrite (tnth_nth (t!_i)) [in X in _ = X](tnth_nth (t!_i)). +rewrite (tnth_nth t!_i) [in X in _ = X](tnth_nth t!_i). by rewrite -(@nth_take k) // -[in X in _ = X](@nth_take k) // tv. Qed.