+<xsl:template mode="eq_transitive" match="*">
+ <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
+ <xsl:choose>
+ <xsl:when test="name()='APPLY'">
+ <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
+ <xsl:variable name="id" select="@id"/>
+ <xsl:choose>
+ <!-- ricordarsi di trattare il parametro -->
+ <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+ <!-- <m:ci>eccomi-3</m:ci> -->
+ <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
+ <xsl:apply-templates mode="noannot" select="*[4]"/>
+ <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="."/>
+ <xsl:with-param name="show_statement" select="0"/>
+ </xsl:call-template>
+ </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>