There is a point in proving
Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).
from this tutorial in Coq where I am stuck. This is the case when False
is left to prove as "False cannot be proven". How do I cope with that?
Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).
Proof.
intros A.
unfold iff.
refine (conj _ _).
case A.
simpl.
intros H.
destruct H.
intros H.
simpl in H.
simpl.
unfold not.
intros.
exact H0.
unfold not.
intros H.
case A.
simpl.
destruct H.
case A.
simpl.
exact I.
simpl.
Focus 2.
simpl.
exact I.
I think I just missed some little important thing in the tutorial.