P → ¬¬P
Demostrar con Lean4 que \(P → ¬¬P\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable (P : Prop) example (h : P) : ¬¬P := by sorry |
Demostrar con Lean4 que \(P → ¬¬P\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Tactic variable (P : Prop) example (h : P) : ¬¬P := by sorry |