diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out
index 7daf828ee..30a839e56 100644
--- a/tests/lean/elab4.lean.expected.out
+++ b/tests/lean/elab4.lean.expected.out
@@ -12,7 +12,7 @@ Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (
     A' :=
     D H
 Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
-    (B a) = (B' (C::explicit A A' (D::explicit A A' B B' H) a))
+    (B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
 Definition R::explicit (A A' : Type)
     (B : A → Type)
     (B' : A' → Type)
@@ -20,4 +20,4 @@ Definition R::explicit (A A' : Type)
     (a : A) : (B a) = (B' (C (D H) a)) :=
     R H a
 Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
-    R::explicit A1 A2 (λ a : A1, B1) (λ _ : A2, B2) H a
+    R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out
index 056ca83c3..30a839e56 100644
--- a/tests/lean/elab5.lean.expected.out
+++ b/tests/lean/elab5.lean.expected.out
@@ -12,7 +12,7 @@ Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (
     A' :=
     D H
 Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
-    (B a) = (B' (C::explicit A A' (D::explicit A A' B B' H) a))
+    (B a) = (B' (C::explicit A A' (D::explicit A A' (λ x : A, B x) (λ x : A', B' x) H) a))
 Definition R::explicit (A A' : Type)
     (B : A → Type)
     (B' : A' → Type)
@@ -20,4 +20,4 @@ Definition R::explicit (A A' : Type)
     (a : A) : (B a) = (B' (C (D H) a)) :=
     R H a
 Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
-    R::explicit A1 A2 (λ _ : A1, B1) (λ _ : A2, B2) H a
+    R::explicit A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a