<?xml version="1.0" encoding="UTF-8"?>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" base="file:/home/aivaras/Hets-src/Framework/specs/logics/propositional/syntax/derived.elf">
<!-- generated by Twelf -->
<import from="?Base"/>
<import from="?CONJ"/>
<import from="?IMP"/>
<constant name="equiv" role="constructor">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMS module="Base" name="o"/>
<om:OMA>
<om:OMS module="Base" name="o"/>
<om:OMS module="Base" name="o"/>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMV name="a">
<type>
<om:OMS module="Base" name="o"/>
</type>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="omitted"/><om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="omitted"/></om:OMV>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMV name="b">
<type>
<om:OMS module="Base" name="o"/>
</type>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="omitted"/><om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="omitted"/></om:OMV>
</om:OMBVAR>
<om:OMA>
<om:OMS module="CONJ" name="and"/>
<om:OMA>
<om:OMS module="IMP" name="imp"/>
<om:OMV name="a"/>
<om:OMV name="b"/>
</om:OMA>
<om:OMA>
<om:OMS module="IMP" name="imp"/>
<om:OMV name="b"/>
<om:OMV name="a"/>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??equiv" role="application" fixity="in" associativity="left" precedence="5" implicit="0"/>
</theory>
</omdoc>