To write mathematical formula, you use other connective that just
universal quantification (
) and implication (
). Oher
symbols are defined in the library prop.phx which is always
loaded when you start . This library and others are described in
the ``User's manual of the library''.