(pred y : bb)

(pred y : bb * bb)

(pred y : bb * bb) (a, b)

(pred y : bb * bb) a b

a =e= < b

a #= e = b

exists1 (predy :: bb)

exists predy:bb . a

exists! a:v . x

exists! a:v . x

exists! a:v . x

forall a:v . x

(a) if (b)

def x

def #

{} when [] else {}

(a) /\ (b) /\ (c)

(a) \/ (b) \/ (c)

(a) => (b)

(a) <=> (b)

true

false

b in s

a =e= b

a = b

(a) => (b) => (c) => (d)

(a) if (b) if (c) if (d)

(a) <=> (b)

(a) /\ (b) if (b) \/ (c) if not c if def d

m div n = r <=> exists s:Nat . m = n * r + s /\ (s < n)