\BOOKMARK [1][-]{section.1}{Introduction}{}
\BOOKMARK [1][-]{section.2}{Notation}{}
\BOOKMARK [2][-]{subsection.2.1}{Hiding construct}{section.2}
\BOOKMARK [2][-]{subsection.2.2}{Metaquantification}{section.2}
\BOOKMARK [2][-]{subsection.2.3}{The `Arbitrary' proof constructor}{section.2}
\BOOKMARK [2][-]{subsection.2.4}{Macro indentation}{section.2}
\BOOKMARK [2][-]{subsection.2.5}{Protected macro expansion}{section.2}
\BOOKMARK [2][-]{subsection.2.6}{Object quantification}{section.2}
\BOOKMARK [2][-]{subsection.2.7}{Proof constructs}{section.2}
\BOOKMARK [2][-]{subsection.2.8}{Modus ponens at the object level}{section.2}
\BOOKMARK [1][-]{section.3}{Side conditions}{}
\BOOKMARK [2][-]{subsection.3.1}{Logiweb terms}{section.3}
\BOOKMARK [2][-]{subsection.3.2}{Deduction}{section.3}
\BOOKMARK [2][-]{subsection.3.3}{Avoidance}{section.3}
\BOOKMARK [2][-]{subsection.3.4}{Substition}{section.3}
\BOOKMARK [1][-]{section.4}{Proofs}{}
\BOOKMARK [2][-]{subsection.4.1}{Proofs of FOL axioms using the inference of deduction}{section.4}
\BOOKMARK [2][-]{subsection.4.2}{A proof of \040x + y = y + x}{section.4}