(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)

a => (b if c)

a if (b => c)

(a => b) if c

(a if b) => c