Can someone help me in proving this using coq script ((q -> p) -> p) -> ((p -> q) -> q) ?

I tried using the identity a -> b = ~ a \/ b but couldn't proceed further.

Coq doesn't generally support "identities" of properties like the one you suggested. You can either add more axioms (e.g., an incarnation of the law of excluded middle) or reformulate the theorem to be about booleans if you want to use `(a -> b) <-> (~ a \/ b) `

Last updated: Jun 25 2024 at 15:02 UTC