liamoc.net
my forest
1\date{2025-11-25T20:14:40Z}
2\author{liamoc}
3\title{Universal Quantifiers}
4\taxon{Definition}
5\parent{isa-0002}
6\import{shiki-macros}
7\put\shiki/language{Isabelle Theory}
8
9\shiki{axiomatization
10 All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10)
11where
12 allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and
13 spec : ‹∀ a. P a ⟹ P x›
14}