@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!
waynee95 has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC