I want to prove A /\ B /\ C /\ D /\ E /\ F in Isabelle. How can I split the subgoal to 6 separate subgoals automatically in proof(rule ...), so then I can prove them separately afterwards?
Of course, I can write proof(rule conjI) 5 times, but maybe there is a more elegant way to do splitting in one step?
Use the intro method: proof (intro conjI)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With