From 4e911765eb80e45ad2a3d2db96f05a284864ed32 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Aug 2022 21:33:56 -0700
Subject: [PATCH] chore: unused vars

---
 src/Lean/Meta/CongrTheorems.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index b9a17a6c32..49d824baf9 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -53,8 +53,8 @@ private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalConte
 
 partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do
   let fType ← inferType f
-  forallBoundedTelescope fType numArgs fun xs xType =>
-  forallBoundedTelescope fType numArgs fun ys yType => do
+  forallBoundedTelescope fType numArgs fun xs _ =>
+  forallBoundedTelescope fType numArgs fun ys _ => do
     if xs.size != numArgs then
       throwError "failed to generate hcongr theorem, insufficient number of arguments"
     else