Faulty translation of Nat existentials into SMT

[dranov]

import Auto
set_option auto.smt true
set_option auto.smt.trust true

set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true

example : false = true := by
  auto -- z3 says Sat

example : ∃ (n : Int), false = true := by
  auto -- z3 says Sat

example : ∃ (n : Nat), false = true := by
  auto -- z3 says Unsat
  /-
  [auto.smt.printCommands] (assert (! (|not| (exists ((|smtd_0| |Int|)) (|=>| (|>=| |smtd_0| 0) (|=| |false| |true|)))) :named valid_fact_0))
  [auto.smt.result] z3 says Unsat, unsat core:
      (|valid_fact_0|)
  -/

In the translation of exists, there should be a conjunction rather than implication. As far as I can tell, the bug is due to lamQuantified2STerm.