diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/Classical_Prop.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 6af7b1fe6e..9c47b73193 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -26,6 +26,8 @@ unfold not; intros; elim (classic p); auto. intro NP; elim (H NP). Qed. +Register NNPP as core.nnpp.type. + (** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P]. Thanks to [forall P, False -> P], it is equivalent to the following form *) |