Stream: General

Topic: Destruction of premises with universal quantification


view this post on Zulip 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: Aug 15 2022 at 02:13 UTC