(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

(b) => (a)

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)

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

(a) <=> (b)

def d => not c => (b) \/ (c) => (a) /\ (b)

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