Finite Field
30-sec diagnosis
Back to NPA

Declaration

not_intro

Mathlib.Logic.Iff

Packages

2

Module

63

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Statement

forall (P : Prop), forall (h : forall (p : P), False), Not P

Proof term

fun P => fun h => h

Constants

Mathlib.Logic.Iff.False

Interface hash: sha256:d9ca31ab11c822de78350f077307aa8ad9671d60cfb6d77584b33bdc4286c11b

Mathlib.Logic.Iff.Not

Interface hash: sha256:e2a4a4c5eb00336cb3f1318ac11972d6d1feaae5e9b54865be4ce0115e989c6c