DeZero.false_elim

Énoncé

∀ {c : Prop} (h : False), c

D’une contradiction, on tire n’importe quelle conclusion.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

/-- Élimination de `False` : d'une contradiction on tire n'importe quelle proposition. -/
theorem false_elim {c : Prop} (h : False) : c :=
  False.rec (motive := fun _ => c) h