Stream: General

Topic: Destruction of premises with universal quantification

Wolfgang Jeltsch (Dec 30 2021 at 13:58):

Is there a way to apply destruction rules to premises involving universal quantification at the outer level? For example, if I have a goal (⋀x. P x ∧ Q x) ⟹ R, can I turn it into (⋀x. P x) ⟹ R using conjunct1?

Last updated: Nov 07 2025 at 16:23 UTC