<?xml version="1.0" encoding="UTF-8"?>

<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" >

<theory name="FalsityPFExt">

<include from="modules.omdoc?FalsityPF"/>

<constant name="falseE'">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMS base="/syntax/modules.omdoc" module="Falsity" name="false"/>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMS base="/syntax/modules.omdoc" module="Falsity" name="false"/>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="FalsityPF" name="falseE"/>

<om:OMV name="p"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??falseE'" role="application" implicit="1"/>

</theory>

<theory name="NEGPFExt">

<include from="modules.omdoc?NEGPF"/>

<constant name="notE'">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="q"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="NEGPF" name="notE"/>

<om:OMV name="A"/>

<om:OMV name="q"/>

<om:OMV name="p"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??notE'" role="application" implicit="2"/>

<constant name="nn">

<type>

<om:OMOBJ>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMA>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="x"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="x"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<constant name="notnotI">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS name="nn"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="NEGPF" name="notI"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="q"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="x"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS name="notE'"/>

<om:OMV name="A"/>

<om:OMV name="x"/>

<om:OMV name="p"/>

<om:OMV name="q"/>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??notnotI" role="application" implicit="1"/>

<constant name="int_notnotE">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS name="nn"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS name="nn"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="NEG" name="not"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="NEGPF" name="notI"/>

<om:OMV name="A"/>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMATP><om:OMV name="q"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="x"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS name="notE'"/>

<om:OMA>

<om:OMS name="nn"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMV name="x"/>

<om:OMA>

<om:OMS name="notnotI"/>

<om:OMV name="A"/>

<om:OMV name="q"/>

</om:OMA>

<om:OMV name="p"/>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??int_notnotE" role="application" implicit="1"/>

</theory>

<theory name="IMPPFExt">

<include from="modules.omdoc?IMPPF"/>

<constant name="imp2I">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="A"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="f"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="IMPPF" name="impI"/>

<om:OMV name="A"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

</om:OMA>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="IMPPF" name="impI"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMATP><om:OMV name="q"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMV name="f"/>

<om:OMV name="p"/>

<om:OMV name="q"/>

</om:OMA>

</om:OMBIND>

</om:OMA>

</om:OMBIND>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??imp2I" role="application" implicit="3"/>

<constant name="imp2E">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="A"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="A"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMATP><om:OMV name="q"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMATP><om:OMV name="r"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="IMPPF" name="impE"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

<om:OMA>

<om:OMS base="modules.omdoc" module="IMPPF" name="impE"/>

<om:OMV name="A"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="IMP" name="imp"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

</om:OMA>

<om:OMV name="p"/>

<om:OMV name="q"/>

</om:OMA>

<om:OMV name="r"/>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??imp2E" role="application" implicit="3"/>

</theory>

<theory name="CONJPFExt">

<include from="modules.omdoc?CONJPF"/>

<constant name="and3I">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="C"/>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMATP><om:OMV name="q"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMATP><om:OMV name="r"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andI"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andI"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

<om:OMV name="p"/>

<om:OMV name="q"/>

</om:OMA>

<om:OMV name="r"/>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??and3I" role="application" implicit="3"/>

<constant name="and3El">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andEl"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andEl"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

<om:OMV name="p"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??and3El" role="application" implicit="3"/>

<constant name="and3Em">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andEr"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andEl"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

<om:OMV name="p"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??and3Em" role="application" implicit="3"/>

<constant name="and3Er">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="x"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andEr"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

<om:OMV name="x"/>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??and3Er" role="application" implicit="3"/>

<constant name="and_comm">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="B"/>

<om:OMV name="A"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

</om:OMA>

</om:OMATP><om:OMV name="p"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andI"/>

<om:OMV name="B"/>

<om:OMV name="A"/>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andEr"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

<om:OMV name="p"/>

</om:OMA>

<om:OMA>

<om:OMS base="modules.omdoc" module="CONJPF" name="andEl"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

<om:OMV name="p"/>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</definition>

</constant>

<notation for="??and_comm" role="application" implicit="2"/>

<constant name="and_assl">

<type>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMA>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMV name="B"/>

</om:OMA>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

<om:OMA>

<om:OMS base="/syntax/base.omdoc" module="Base" name="ded"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="A"/>

<om:OMA>

<om:OMS base="/syntax/modules.omdoc" module="CONJ" name="and"/>

<om:OMV name="B"/>

<om:OMV name="C"/>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMA>

</om:OMBIND>

</om:OMBIND>

</om:OMBIND>

</om:OMOBJ>

</type>

<definition>

<om:OMOBJ>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="A"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="B"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_lambda"/>

<om:OMBVAR>

<om:OMATTR><om:OMATP>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>

<om:OMS base="/syntax/base.omdoc" module="Base" name="o"/>

</om:OMATP><om:OMV name="C"/>

</om:OMATTR>

</om:OMBVAR>

<om:OMBIND>

<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>