On Negation (impredicative definition)

Consider the following definitions :

Definition my_False : Prop := forall P:Prop, P.

Definition my_not (P:Prop) : Prop := P -> my_False.

Prove the same theorems as in that exercise , but using my_False and my_not instead of False and not.

Solution