diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean
index 03e9479..382390a 100644
--- a/Auto/Translation/LamFOL2SMT.lean
+++ b/Auto/Translation/LamFOL2SMT.lean
@@ -297,7 +297,8 @@ def lamQuantified2STerm (forall? : Bool) (s : LamSort) (body : TransM LamAtom ST
   let dname ← disposableName
   let mut body' ← body
   if s == .base .nat then
-    body' := .qStrApp "=>" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body']
+    let connective := if forall? then "=>" else "and"
+    body' := .qStrApp connective #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body']
   match forall? with
   | true => return .forallE dname s' body'
   | false => return .existE dname s' body'