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: Feb 01 2023 at 11:04 UTC