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