3 ms·

The "let" should really be read as "for all". If you do so, your objection disappears since quantifying over the empty always imply the consequent.

• tel 11y ago
  You also need to translate "with" as a forall (pi binder) as well. Then, you'll merely note that the formula is unsatisfiable without demonstrating a proof that y is within the proper bounds.
  • eli_gottlieb 11y ago
    Oh good, so I'm not the only one whose mind tries to translate mathematical prose into the notation of dependent type theory!
    • tel 11y ago
      Sometimes your problem really does just call for a hammer :)