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: Apr 25 2024 at 16:19 UTC