Prove the following propositions:
forall P:Prop, ~ ~ ~ P -> ~ P
forall P Q:Prop, ~ ~ ~ P -> P -> Q
forall P Q:Prop, (P -> Q) -> ~ Q -> ~ P.
forall P Q R:Prop, (P -> Q) -> (P -> ~ Q) -> P -> R.
Some of these propositions don't need False-elimination;
in these situations, show that these theorems are derived from some
theorems of the minimal propositional logic.
Whenever False-elimination is not
needed, we first proved some lemma in minimal propositional logic, then
apply it to derive the statement we wanted to prove.
Please notice that all these results could be proved in one step :
either by "unfold not; auto" if False-elimination is not needed,
or by tauto in the other case.