chore: add not_not_intro

leodemoura · leodemoura · commit 8d90872d284d · 2021-08-17T21:32:32.000-07:00
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
@@ -180,6 +180,9 @@ theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=
 
 theorem not_false : ¬False := id
 
+theorem not_not_intro {p : Prop} (h : p) : ¬ ¬ p :=
+  fun hn : ¬ p => hn h
+
 -- proof irrelevance is built in
 theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
 
