+<xsl:template match="target" mode="letin">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+<!--xsl:template match="PROD" mode="pure">
+ <xsl:for-each select="decl">
+ <m:apply helm:xref="{@id}">
+ <xsl:choose>
+ <xsl:when test="string(@binder)= """>
+ <m:csymbol>arrow</m:csymbol>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:choose>
+ <xsl:when test="../@type = 'Prop'">
+ <m:csymbol>forall</m:csymbol>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:csymbol>prod</m:csymbol>
+ </xsl:otherwise>
+ </xsl:choose>
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
+ </xsl:otherwise>
+ </xsl:choose>
+ </m:apply>
+ </xsl:for-each>
+ <xsl:apply-templates select="target/*[1]" mode="noannot"/>
+</xsl:template-->
+
+<xsl:template match="PROD" mode="pure">
+ <xsl:apply-templates select="*[1]" mode="prod"/>
+</xsl:template>
+
+<xsl:template match="decl" mode="prod">
+ <m:apply helm:xref="{@id}">
+ <xsl:choose>
+ <xsl:when test="string(@binder)= """>
+ <m:csymbol>arrow</m:csymbol>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:choose>
+ <xsl:when test="../@type = 'Prop'">
+ <m:csymbol>forall</m:csymbol>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:csymbol>prod</m:csymbol>
+ </xsl:otherwise>
+ </xsl:choose>
+ <m:bvar>
+ <m:ci>
+ <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+ </m:ci>
+ <m:type>
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+ </m:type>
+ </m:bvar>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates select="following-sibling::*[1]" mode="prod"/>
+ </m:apply>
+</xsl:template>
+
+
+<xsl:template match="target" mode="prod">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+