Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	set-basic	f	Set[A] → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. ++ .	set-basic	f	Set[A] × A → Set[A]
. +1	nat-basic	f	Nat → Nat
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. < .	nat-basic	p	Nat × Nat
. > .	nat	p	Nat × Nat
. ∈ .	set-basic	p	'A × Set('A)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	set-basic	p	Set('A) × Set('A)
∅	set-basic	c	Set[A]
Nat	nat-basic	s
Set	set-basic	s
a	set-basic	v	A
b	set-basic	v	A
n	set-basic	v	Nat
s	set-basic	v	Set[A]