4 ms·

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

by 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 :)