bug fix

leanprover-community · Sep 28, 2024 · 28543ee · 28543ee
1 parent 45fc6c6
commit 28543ee
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean
@@ -1161,7 +1161,7 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do
       if name == ``Embedding.forallF then
         let [lvl₁, lvl₂] := lvls
           | throwError "processSimpleApp :: Auto.Embedding.forallF should have two levels"
-        if !(← Meta.isLevelDefEq lvl₁ .zero) || !(← Meta.isLevelDefEq lvl₂ .zero) then
+        if !(← Meta.isLevelDefEq lvl₂ .zero) then
           return .none
       return .some (.base (tcon (← reifType arg)))
     return .none