∀ {env : Lean.Kernel.Environment} {name : Lean.Name} {expr : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {name_1 : Lean.Name} {expr_1 : Lean.Expr},
  Lean.Kernel.Exception.declHasMVars env name expr = Lean.Kernel.Exception.declHasMVars env_1 name_1 expr_1 →
    env = env_1 ∧ name = name_1 ∧ expr = expr_1