Stream: Beginner Questions

Topic: Don't split implications in `safe`

view this post on Zulip Hanno Becker (Feb 23 2023 at 14:57):

Hi. How can I prevent safe from splitting a subgoal with assumption P --> Q into two subgoals with assumption not(P) and Q, respectively?

view this post on Zulip Lukas Stevens (Feb 23 2023 at 16:12):

apply(safe del: impCE)

view this post on Zulip Lukas Stevens (Feb 23 2023 at 16:14):

I found the offending rule by searching through the set of known classical rules that print_claset spits out.

view this post on Zulip Hanno Becker (Feb 23 2023 at 19:45):

Awesome, thank you!

Last updated: Jun 26 2026 at 21:20 UTC