+ </xsl:when>
+ <xsl:otherwise>
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>or_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[7]"/>
+ <xsl:apply-templates mode="pure"
+ select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+ <xsl:apply-templates mode="pure" select="*[5]"/>
+ <xsl:apply-templates mode="pure" select="*[6]"/>
+ </m:apply>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <!-- ex_ind, exT_ind -->
+ <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
+ CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
+ and count(child::*) = 6
+ and name(*[5])='LAMBDA'
+ and name(*[5]/target/*[1])='LAMBDA'">
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>ex_ind</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="*[6]"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
+ <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+ <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
+ <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:when test="name(*[1])='CONST'">
+ <xsl:apply-templates mode="try_inductive" select="."/>
+ </xsl:when>
+ <!-- patch temporanea per la gestione di redex -->
+ <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
+ and *[2]/@sort='Prop'">
+ <m:apply helm:xref="{@id}">
+ <m:csymbol>letin</m:csymbol>
+ <m:apply>
+ <m:csymbol>let</m:csymbol>
+ <m:ci>
+ <xsl:call-template name="insert_subscript">
+ <xsl:with-param name="node_value">
+ <xsl:value-of select="*[1]/target/@binder"/>
+ </xsl:with-param>
+ </xsl:call-template>
+ </m:ci>
+ <xsl:apply-templates mode="noannot" select="*[2]"/>
+ </m:apply>
+ <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="." mode="letin"/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
+ <xsl:when test="name()='LAMBDA'">
+ <xsl:choose>
+ <xsl:when test="(name(target/*[1])='APPLY' and
+ name(target/*[1]/*[1])='CONST' and
+ (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
+ and count(target/*[1]/*) = 8
+ and name(target/*[1]/*[8])='REL'
+ and target/@binder = target/*[1]/*[8]/@binder )">
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
+ <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
+ <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
+ <xsl:call-template name="generate_side_proof">
+ <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
+ </xsl:call-template>
+ <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
+ </m:apply>