Stream: Beginner Questions

Topic: Knowing what rule apply (rule) used

Ant S. (Sep 24 2026 at 07:26):

Suppose I have a proof script

have X: (∀x <= N. ∀y <= M. ...)
proof (rule, rule, rule ...)

applying rule like this seems clunky (to get rid of HOL-level quantifiers and implications from the quantifier) and I assume there's a much more elegant way to do this.

So a. What's the more elegant way to clean up HOL level quantifiers like these, if any.
and b. How do I know what rule rule used?

Last updated: Sep 28 2026 at 16:33 UTC