English
In the logic of propositions, for any predicate f on propositions, the universal quantification (over all p) of f(p) is equivalent to f(True) and f(False).
Русский
В логике высказываний для любого предиката f на propositions справедливо, что ∀ p, f(p) эквивалентно f(True) и f(False).
LaTeX
$$$ \forall {a,b,c \in \mathrm{Prop}}, \big( (a \leftrightarrow (b \leftrightarrow c)) \big) \iff \big( a \leftrightarrow (b \leftrightarrow c) \big) $$$
Lean4
theorem «forall» {f : Prop → Prop} : (∀ p, f p) ↔ f True ∧ f False :=
⟨fun h ↦ ⟨h _, h _⟩, by rintro ⟨h₁, h₀⟩ p; by_cases hp : p <;> simp only [hp] <;> assumption⟩
