waynee95 (Dec 13 2022 at 20:48): waynee95 (Dec 13 2022 at 20:48):@Simon Roßkopf I see. I always wondered why I sometimes saw using assms in other proofs. So far I have only been using [| P|] ==> Q notation for proofs and I thought that the former is just syntactic sugar for the latter but they handle proof state differently, which I didn't know. Thanks!
Notification Bot (Dec 13 2022 at 20:48):waynee95 has marked this topic as resolved.
Last updated: Apr 25 2024 at 04:18 UTC