improvement

Beluga-lang · Oct 16, 2024 · 6d99564 · 6d99564
1 parent dd6e0b7
commit 6d99564
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Core/Soundness/NatCases.v b/theories/Core/Soundness/NatCases.v
@@ -402,7 +402,7 @@ Proof.
   assert {{ ⊢ Δ, ℕ }} by mauto 3.
   assert {{ Δ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3.
   assert {{ ⊢ Δ, ℕ, A[q σ] }} by mauto 2.
-  unshelve assert {{ Δ ⊢ M : ℕ }} by mauto 3; [constructor |].
+  assert {{ Δ ⊢ M : ℕ }} by mautosolve 3.
   assert {{ Δ ⊢ ℕ : Type@0 }} by mauto 3.
   assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} by mauto 3.
   assert {{ Δ ⊢ M : ℕ[σ] }} by mauto 3.