From edeecdcf2cb51318a7d4c608652f4f988e80f66f Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 2 Dec 2002 09:29:12 +0000
Subject: [PATCH] *** empty log message ***

---
 helm/style/content.xsl         |  27 +-
 helm/style/content_to_html.xsl | 133 +++++-
 helm/style/diseq.xsl           | 336 ++++++++++++++
 helm/style/drop_coercions.xsl  |  22 +-
 helm/style/headercontent.xsl   |   1 +
 helm/style/inductive.xsl       | 361 +++++++--------
 helm/style/logic.xsl           | 138 ++++++
 helm/style/objcontent.xsl      |   6 +-
 helm/style/params.xsl          |  23 +-
 helm/style/proofs.xsl          | 788 +++++++--------------------------
 helm/style/rewrite.xsl         | 135 ++++++
 helm/style/rootcontent.xsl     |  10 +-
 helm/style/xslt_index.txt      |   3 +
 13 files changed, 1157 insertions(+), 826 deletions(-)
 create mode 100644 helm/style/diseq.xsl
 create mode 100644 helm/style/logic.xsl
 create mode 100644 helm/style/rewrite.xsl

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index 9aea96b3c..e47126138 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -88,11 +88,13 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 
 <xsl:template match="LETIN" mode="pure">
-	<xsl:apply-templates select="*[1]" mode="letin"/>
+	<xsl:apply-templates select="*[1]" mode="letin_pure"/>
 </xsl:template>
 
+<!-- Andrea: mode letin already exists in proofs.xsl, with a 
+    different meaning -->
 
-<xsl:template match="def" mode="letin">	
+<xsl:template match="def" mode="letin_pure">	
     <m:apply helm:xref="{@id}">
      <m:csymbol>let_in</m:csymbol>
      <m:bvar>
@@ -101,12 +103,12 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
       </m:ci>
      </m:bvar>
      <xsl:apply-templates select="*[1]" mode="noannot"/>
-     <xsl:apply-templates select="following-sibling::*[1]" mode="letin"/>
+     <xsl:apply-templates select="following-sibling::*[1]" mode="letin_pure"/>
     </m:apply>
 </xsl:template>
 
 
-<xsl:template match="target" mode="letin">
+<xsl:template match="target" mode="letin_pure">
 	<xsl:apply-templates select="*[1]" mode="noannot"/>
 </xsl:template>
 
@@ -326,7 +328,22 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 	 <m:csymbol>inst</m:csymbol>
 	 <xsl:apply-templates mode="noannot" select="*[1]" />
 	 <xsl:for-each select="arg">
-	  <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:with-param></xsl:call-template></m:ci>
+          <xsl:variable name="base_path">
+           <xsl:call-template name="path">
+            <xsl:with-param name="uri" select="../*[1]/@uri"/>
+           </xsl:call-template>
+          </xsl:variable>
+          <xsl:variable name="varUri" select="concat($base_path,@relUri)"/>
+	  <m:ci definitionURL="{$varUri}">
+           <xsl:call-template name="insert_subscript">
+            <xsl:with-param name="node_value">
+             <xsl:call-template name="name_of_uri">
+              <xsl:with-param name="uri" select="$varUri"/>
+              <xsl:with-param name="extension" select="'.var'"/>
+             </xsl:call-template>
+            </xsl:with-param>
+           </xsl:call-template>
+          </m:ci>
 	  <xsl:apply-templates mode ="noannot" select="*[1]" />
 	 </xsl:for-each>
 	</m:apply>
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 2fb4aa533..21b663942 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -69,6 +69,12 @@
    <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
     <xsl:variable name="fontsymbol">
      <xsl:choose>
+      <xsl:when test="$symbol = 'append'">
+       <xsl:value-of select="'@'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'iff'">
+       <xsl:value-of select="'&#xAB;'"/>
+      </xsl:when>
       <xsl:when test="$symbol = 'forall'">
        <xsl:value-of select="'&#x22;'"/>
       </xsl:when>
@@ -114,6 +120,12 @@
    <xsl:otherwise>
     <xsl:variable name="unicodesymbol">
      <xsl:choose>
+      <xsl:when test="$symbol = 'append'">
+       <xsl:value-of select="'@'"/>
+      </xsl:when>
+      <xsl:when test="$symbol = 'iff'">
+       <xsl:value-of select="'&#x2194;'"/>
+      </xsl:when>
       <xsl:when test="$symbol = 'forall'">
        <xsl:value-of select="'&#8704;'"/>
       </xsl:when>
@@ -311,6 +323,30 @@
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
      <xsl:text>)</xsl:text>
     </xsl:when>
+    <!-- IFF -->
+    <xsl:when test="$name='iff'">
+     <xsl:text>(</xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+     <xsl:call-template name="mksymbol-1">
+      <xsl:with-param name="symbol" select="$name"/>
+      <xsl:with-param name="color" select="'blue'"/>
+      <xsl:with-param name="size" select="'+0'"/>
+     </xsl:call-template>
+     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+     <xsl:text>)</xsl:text>
+    </xsl:when>
+    <!-- APPEND -->
+    <xsl:when test="$name='append'">
+     <xsl:text>(</xsl:text>
+     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+     <xsl:call-template name="mksymbol-1">
+      <xsl:with-param name="symbol" select="$name"/>
+      <xsl:with-param name="color" select="'blue'"/>
+      <xsl:with-param name="size" select="'+0'"/>
+     </xsl:call-template>
+     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
+     <xsl:text>)</xsl:text>
+    </xsl:when>
     <!-- APP -->
     <xsl:when test="$name='app'">
      <xsl:text>(</xsl:text>
@@ -365,12 +401,21 @@
     </xsl:when>
     
     <xsl:when test="$name='inst'">
-     <xsl:apply-templates select="*[1]" mode="inline"/>
+     <xsl:apply-templates select="*[2]" mode="inline"/>
      <FONT color="blue">{</FONT>
-     <xsl:text>trjsh</xsl:text>
-     <xsl:apply-templates select="*[2]" mode="args"/>
+     <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+      <xsl:apply-templates select="following-sibling::*[position() = 1]" mode="inline"/>
+      <FONT color="blue">/</FONT> 
+      <xsl:if test="name()='m:ci'">
+       <a href="{@definitionURL}">
+        <xsl:apply-templates/>
+       </a>
+      </xsl:if>
+      <!-- <xsl:apply-templates select="." mode="inline"/> -->
+     </xsl:for-each>
      <FONT color="blue">}</FONT>
     </xsl:when>
+
     <!-- FIX -->
     <xsl:when test="$name='fix'">
      <FONT color="red">FIX</FONT>
@@ -776,6 +821,10 @@
      <!-- <xsl:value-of select="$charlength"/> -->
   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
      <xsl:choose>
+     <!-- inst -->
+      <xsl:when test="$name='inst'">
+       <xsl:apply-templates select="." mode="inline"/>
+      </xsl:when>
      <!-- FORALL -->
       <xsl:when test="$name='forall'">
        <xsl:choose>
@@ -862,6 +911,62 @@
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- IFF -->
+      <xsl:when test="$name='iff'">
+       <xsl:choose>
+       <xsl:when test="$charlength > $framewidth">
+       <xsl:text>(</xsl:text>
+       <xsl:apply-templates select="*[position()=2]">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <!-- -> -->
+       <xsl:call-template name="mksymbol-1">
+        <xsl:with-param name="symbol" select="$name"/>
+        <xsl:with-param name="color" select="'blue'"/>
+        <xsl:with-param name="size" select="'+0'"/>
+       </xsl:call-template>
+       <xsl:apply-templates select="*[position()=3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+       </xsl:apply-templates>
+       <xsl:text>)</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:apply-templates mode="inline" select="."/>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <!-- APPEND -->
+      <xsl:when test="$name='append'">
+       <xsl:choose>
+       <xsl:when test="$charlength > $framewidth">
+       <xsl:text>(</xsl:text>
+       <xsl:apply-templates select="*[position()=2]">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <!-- -> -->
+       <xsl:call-template name="mksymbol-1">
+        <xsl:with-param name="symbol" select="$name"/>
+        <xsl:with-param name="color" select="'blue'"/>
+        <xsl:with-param name="size" select="'+0'"/>
+       </xsl:call-template>
+       <xsl:apply-templates select="*[position()=3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+       </xsl:apply-templates>
+       <xsl:text>)</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:apply-templates mode="inline" select="."/>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
       <!-- APP -->
       <xsl:when test="$name='app'">
        <xsl:choose>
@@ -1097,6 +1202,24 @@
          <xsl:with-param name="current_indent" select="$current_indent"/>
         </xsl:apply-templates>
         &#x00a0;
+        <xsl:if test="*[4]">
+         <br/>
+         <xsl:call-template name="make_indent">
+          <xsl:with-param name="current_indent" select="$current_indent"/>
+         </xsl:call-template>
+         <FONT color="red">we proved&#x00a0;</FONT>
+         <xsl:apply-templates select="*[position()=3]">
+          <xsl:with-param name="current_indent" select="$current_indent+16"/>
+         </xsl:apply-templates>
+         <br/>
+         <xsl:call-template name="make_indent">
+          <xsl:with-param name="current_indent" select="$current_indent"/>
+         </xsl:call-template>
+         <FONT color="red">and by delta equivalence</FONT>
+         <xsl:apply-templates select="*[position()=5]">
+          <xsl:with-param name="current_indent" select="$current_indent+16"/>
+         </xsl:apply-templates>
+       </xsl:if>
        </span>
        <xsl:choose>
         <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
@@ -1120,7 +1243,7 @@
              <xsl:call-template name="make_indent">
               <xsl:with-param name="current_indent" select="$current_indent"/>
              </xsl:call-template>\
-             <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we proved</a>\
+             <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we obtain</a>\
             </span>\
            ');
            document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
@@ -1138,7 +1261,7 @@
          </script>
         </xsl:otherwise>
        </xsl:choose>
-       <xsl:apply-templates select="*[position()=3]">
+       <xsl:apply-templates select="*[position()=last()]">
         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
        </xsl:apply-templates>
       </xsl:when>
diff --git a/helm/style/diseq.xsl b/helm/style/diseq.xsl
new file mode 100644
index 000000000..dd3650db7
--- /dev/null
+++ b/helm/style/diseq.xsl
@@ -0,0 +1,336 @@
+<?xml version="1.0"?>
+
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
+<!--******************************************************************--> 
+<!-- Disequalities                                                    -->
+<!-- (completely) Revisited: november 2002, Andrea Asperti            -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm">
+
+<!-- ************************* LOGIC *********************************-->
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'eq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'eq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'eq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'eq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'eq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[5]"/>
+  <xsl:apply-templates mode="diseq" select="*[7]">
+   <xsl:with-param name="rel" select="'eq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[2]"/>
+  <xsl:apply-templates mode="diseq" select="*[5]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply>
+  <m:csymbol>diseq_chain</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[2]"/>
+  <xsl:apply-templates mode="diseq" select="*[5]">
+   <xsl:with-param name="rel" select="'lt'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+  <xsl:apply-templates mode="diseq" select="*[6]">
+   <xsl:with-param name="rel" select="'leq'"/>
+  </xsl:apply-templates>
+  <xsl:apply-templates mode="noannot" select="*[4]"/>
+ </m:apply>
+</xsl:template> 
+
+<xsl:template mode="diseq" match="*">
+ <xsl:param name="rel" select="'eq'"/>
+  <xsl:choose>
+   <xsl:when test="name()='APPLY'">
+    <xsl:variable name="id" select="@id"/>
+    <xsl:choose>
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+     </xsl:when> 
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
+       <xsl:call-template name="generate_side_proof">
+        <xsl:with-param name="proof" select="*[7]"/>
+        <xsl:with-param name="show_statement" select="0"/>
+       </xsl:call-template>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+     </xsl:when> 
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+     </xsl:when>
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+     </xsl:when>  
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+     </xsl:when>  
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
+      <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+     </xsl:when> 
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+     </xsl:when>
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+     </xsl:when>
+     <!-- REALS -->
+     <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6">
+       <xsl:apply-templates mode="diseq" select="*[5]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+     </xsl:when>
+     <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6">
+       <xsl:apply-templates mode="diseq" select="*[5]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:element name="{concat('m:',$rel)}"/>
+      <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:element name="{concat('m:',$rel)}"/> 
+    <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>
+
+
+</xsl:stylesheet>
diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl
index b31160eab..7b1316013 100644
--- a/helm/style/drop_coercions.xsl
+++ b/helm/style/drop_coercions.xsl
@@ -40,18 +40,18 @@
 <!-- coercions -->
 
 <xsl:template match="APPLY[CONST[position()='1' and 
-         (@uri='cic:/Algebra/CSemiGroups/csg_crr.con' or 
-          @uri='cic:/Algebra/CMonoids/cm_crr.con' or
-          @uri='cic:/Algebra/CGroups/cg_crr.con' or
-          @uri='cic:/Algebra/CRings/cr_crr.con' or
-          @uri='cic:/Algebra/CFields/cf_crr.con' or
-          @uri='cic:/Algebra/COrdFields/cof_crr.con' or
-          @uri='cic:/Algebra/CReals/crl_crr.con')]]">
+         (@uri='cic:/Algebra/algebra/CSemiGroups/csg_crr.con' or 
+          @uri='cic:/Algebra/algebra/CMonoids/cm_crr.con' or
+          @uri='cic:/Algebra/algebra/CGroups/cg_crr.con' or
+          @uri='cic:/Algebra/algebra/CRings/cr_crr.con' or
+          @uri='cic:/Algebra/algebra/CFields/cf_crr.con' or
+          @uri='cic:/Algebra/algebra/COrdFields/cof_crr.con' or
+          @uri='cic:/Algebra/reals/CReals/crl_crr.con')]]">
   <xsl:apply-templates select="*[position()=last()]"/>
 </xsl:template>
 
 <xsl:template match="APPLY[CONST[position()='1' and 
-   @uri='cic:/Algebra/CSetoids/CSetoid_functions/csf_fun.con']]">
+   @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csf_fun.con']]">
      <xsl:variable name="no_params">
       <xsl:call-template name="get_no_params">
        <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -84,7 +84,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST[position()='1' and 
-   @uri='cic:/Algebra/CSetoids/CSetoid_functions/csbf_fun.con']]">
+   @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csbf_fun.con']]">
      <xsl:variable name="no_params">
       <xsl:call-template name="get_no_params">
        <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -119,7 +119,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST[position()='1' and 
-   @uri='cic:/Algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
+   @uri='cic:/Algebra/algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]">
      <xsl:variable name="no_params">
       <xsl:call-template name="get_no_params">
        <xsl:with-param name="first_uri" select="$CICURI"/>
@@ -154,7 +154,7 @@
 </xsl:template>
 
 <xsl:template match="APPLY[CONST[position()='1' and 
-   @uri='cic:/Algebra/CRings/nat_injection/nring.con']]">
+   @uri='cic:/Algebra/algebra/CRings/nat_injection/nring.con']]">
      <xsl:variable name="no_params">
       <xsl:call-template name="get_no_params">
        <xsl:with-param name="first_uri" select="$CICURI"/>
diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl
index f60883079..c5151a0d2 100644
--- a/helm/style/headercontent.xsl
+++ b/helm/style/headercontent.xsl
@@ -35,6 +35,7 @@
 <xsl:include href="basic.xsl"/>
 <xsl:include href="arith.xsl"/>        <!-- FG -->
 <xsl:include href="set.xsl"/>
+<xsl:include href="list.xsl"/>
 <xsl:include href="reals.xsl"/>
 <xsl:include href="ring.xsl"/>        <!-- FG -->
 <xsl:include href="algebra.xsl"/> 
diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 83569d751..4066d4be3 100644
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -26,6 +26,7 @@
 
 <!--******************************************************************--> 
 <!-- XSLT version 0.1 of CIC inductive objects to MathML content:     -->
+<!-- Completely revisited: November 2002, Andrea asperti              -->
 <!-- First draft: March 2001, Andrea asperti                          -->
 <!--******************************************************************-->
 
@@ -34,20 +35,75 @@
                               xmlns:m="http://www.w3.org/1998/Math/MathML"
                               xmlns:helm="http://www.cs.unibo.it/helm">
 
+<!-- try_inductive essentially checks if the head constant is an
+     invocation of an induction principle. 
+     Si presuppone che il tipo induttivo non sia mutuamente 
+     induttivo. Bisognerebbe andare a vedere l'utlimo parametro
+     del presunto "principio di induzione", tirare fuori il tipo induttivo
+     e vedere se il suo nome coincide con il prefisso di _ind. 
+     Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
+     parametro di nat_double_ind e' di tipo nat, e nat e' diverso
+     da nat_double. Per ora, verifico solo l'esistenza di nat_double,
+     ma questo, benche' non porti ad errore, non copre tutti i
+     casi per quelli mutuamente induttivi -->
+
+
+<xsl:template mode="try_inductive" match="APPLY">
+ <xsl:variable name="id" select="@id"/>
+  <xsl:choose>
+   <xsl:when test="CONST[1]">
+    <xsl:variable name="uri" select="CONST[1]/@uri"/>
+    <xsl:choose>
+     <xsl:when test="contains($uri,'_ind.con')">
+      <xsl:variable name="ind_uri" 
+        select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
+      <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
+      <xsl:variable name="inductive_def" 
+     select="document($InductiveTypeUrl)/InductiveDefinition"/>
+      <xsl:choose>
+       <xsl:when test="$inductive_def">
+        <xsl:variable name="ind_name">
+         <xsl:call-template name="get_name">
+          <xsl:with-param name="uri" select="$uri"/>
+         </xsl:call-template>
+        </xsl:variable>
+        <xsl:apply-templates mode="inductive" select=".">
+         <xsl:with-param name="inductive_def_uri" 
+          select="$ind_uri"/>
+         <xsl:with-param name="inductive_def" select="$inductive_def"/>
+         <xsl:with-param name="inductive_def_index" select="1"/>
+         <xsl:with-param name="inductive_def_name" select="$ind_name"/>
+        </xsl:apply-templates>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:apply-templates select="." mode="letin"/>
+       </xsl:otherwise>
+      </xsl:choose>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:apply-templates select="." mode="letin"/>
+     </xsl:otherwise>
+    </xsl:choose>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:apply-templates select="." mode="letin"/>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
 
 <xsl:template mode="inductive" match="APPLY">
  <xsl:param name="inductive_def_uri" select="''"/>
  <xsl:param name="inductive_def" select="/.."/>
  <xsl:param name="inductive_def_index" select="1"/>
  <xsl:param name="inductive_def_name" select="''"/>
- <xsl:param name="section_params" select="0"/>
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
  <!-- expected_args_type contains the types of the arguments expected by
       the induction principle -->
- <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
  <xsl:variable name="expected_args_types" 
-	select="document($InductiveTypeUrl)/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
+      select="document($InductiveTypeUrl)/ConstantType/PROD/decl/*[1]"/>
  <xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
- <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
+ <xsl:variable name="actual_arguments" select="*[position()>1]"/>
  <!-- First check that the induction principle is applied to the
       expected number of arguments -->
  <xsl:choose>
@@ -65,7 +121,7 @@
     <xsl:when test="string($argsOK) = 'true'">
      <!-- arguments are in the expected form: we create a
           "by_induction" content element -->
-     <!-- no_params is the number of paramters in square brackets -->
+     <!-- no_params is the number of parameters in square brackets -->
      <xsl:variable name="no_params" 
       select="$inductive_def/@noParams"/>
      <!-- the inductive property is the first argument following
@@ -93,7 +149,7 @@
            is the uri of the inductive definition -->
       <m:ci><xsl:value-of select="$inductive_def_uri"/></m:ci>
       <!-- next, we have the inductive property, currently not
-           used for rendering (it could be omitted??) -->
+           used for rendering (it could be omitted ??) -->
       <xsl:apply-templates mode="pure" select="$inductive_property"/>
       <!-- each case has its own "inductive_case" element -->
       <!-- the inductive case element is composed by:
@@ -117,40 +173,44 @@
          <m:csymbol>case_lhs</m:csymbol>
          <m:ci definitionURL="{$inductive_def_uri}">
           <xsl:value-of select="@name"/>
-         </m:ci>     
+         </m:ci> 
          <xsl:call-template name="get_constructor_args">
-          <xsl:with-param name="no_params" 
-               select="$no_params"/>
-          <xsl:with-param name="constructor_arity" 
-               select="*[1]"/>
-          <xsl:with-param name="actual_arg" 
-               select="$current_arg"/>
-          <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
-          </xsl:call-template>
+          <xsl:with-param name="constructor_args" 
+               select="PROD/decl[position()> $no_params]"/>
+          <xsl:with-param name="actual_args" 
+               select="$current_arg/decl"/>
+          <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
+          </xsl:call-template>  
         </m:apply>
         <m:apply>
          <m:csymbol>induction_hypothesis</m:csymbol>
          <xsl:call-template name="get_induction_hypothesis">
-          <xsl:with-param name="no_params" 
-               select="$no_params"/>
-          <xsl:with-param name="constructor_arity" 
-               select="*[1]"/>
-          <xsl:with-param name="actual_arg" 
-               select="$current_arg"/>
-          <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
+          <xsl:with-param name="constructor_args" 
+               select="PROD/decl[position()> $no_params]"/>
+          <xsl:with-param name="actual_args" 
+               select="$current_arg/decl"/>
+          <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
          </xsl:call-template>
         </m:apply>
-        <xsl:call-template name="get_body">
-         <xsl:with-param name="no_params" 
-               select="$no_params"/>
-         <xsl:with-param name="constructor_arity" 
-               select="*[1]"/>
-         <xsl:with-param name="actual_arg" select="$current_arg"/>
-         <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
-        </xsl:call-template>
+        <xsl:choose>
+         <xsl:when test="count(PROD/decl) > $no_params">
+          <!-- in this case the actual_arg must be a LAMBDA -->
+          <xsl:call-template name="get_body">
+           <xsl:with-param name="constructor_args" 
+               select="PROD/decl[position()>$no_params]"/>
+           <xsl:with-param name="actual_args" select="$current_arg/decl"/>
+           <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
+           <xsl:with-param name="target" 
+               select="$current_arg/target/*[1]"/>
+          </xsl:call-template>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:apply-templates mode="noannot" select="$current_arg"/>
+         </xsl:otherwise>
+        </xsl:choose>
        </m:apply>
       </xsl:for-each>
       <!-- the inductive argument is the last argument of extra-args -->
@@ -179,6 +239,8 @@
      If this is not the case, not good rendering looks possible.
      Check_args returns a boolean. 
    -->
+
+
 <xsl:template name="check_args">
  <xsl:param name="arg_types" select="/.."/>
  <xsl:param name="actual_args" select="/.."/>
@@ -188,17 +250,10 @@
     <xsl:value-of select="$bool_var"/>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:variable name="no_expected_arg_of_arg">
-    <xsl:apply-templates mode="count_arity" select="$arg_types[1]">
-     <xsl:with-param name="what" select="'PROD'"/>
-    </xsl:apply-templates>
-   </xsl:variable>
-   <xsl:variable name="no_actual_abst_of_arg"> 
-    <xsl:apply-templates mode="count_arity" select="$actual_args[1]">
-     <xsl:with-param name="what" select="'LAMBDA'"/>
-    </xsl:apply-templates>
-   </xsl:variable>
-   <!-- REPLACE WITH EQUALITY ???? -->
+   <xsl:variable name="no_expected_arg_of_arg" 
+                 select="count($arg_types[1]/PROD/decl)"/>
+   <xsl:variable name="no_actual_abst_of_arg" 
+                 select="count($actual_args[1]/LAMBDA/decl)"/> 
    <xsl:variable name="test_arg" 
     select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/> 
    <xsl:call-template name="check_args">
@@ -208,25 +263,8 @@
    </xsl:call-template> 
   </xsl:otherwise>
  </xsl:choose>
-</xsl:template>
+</xsl:template> 
 
-<!-- count_arity counts the number of head lambda (or prod) -->
-<xsl:template mode="count_arity" match="*">
- <xsl:param name="what" select="'LAMBDA'"/>
- <xsl:param name="num" select="0"/>
- <!-- MANCANO I CAST ??? -->
- <xsl:choose>
-  <xsl:when test="name(.) = $what">
-   <xsl:apply-templates mode="count_arity" select="target/*[1]">
-    <xsl:with-param name="what" select="$what"/>
-    <xsl:with-param name="num" select="$num+1"/>
-   </xsl:apply-templates>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:value-of select="$num"/>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
 
 <!-- The following three functions are essentially identical
      in their recursive structure.
@@ -246,162 +284,127 @@
      single one without a conversion from document tree fragments
      to node-sets. 
 -->
+
 <xsl:template name="get_constructor_args">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
- <xsl:if test="name($constructor_arity)='PROD'">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:if test="$constructor_args">
   <m:bvar>
-   <m:ci><xsl:value-of select="$actual_arg/target/@binder"/></m:ci>
+   <m:ci><xsl:value-of select="$actual_args[1]/@binder"/></m:ci>
    <m:type>
-    <xsl:apply-templates mode="pure" select="$actual_arg/source/*[1]"/>
+    <xsl:apply-templates mode="pure" select="$actual_args[1]/*"/>
    </m:type> 
   </m:bvar>
   <xsl:choose>
-   <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+   <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
     <xsl:call-template name="get_constructor_args">
     <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg/target/LAMBDA/target/*[1]"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
+        select="$constructor_args[position()>1]"/>
+    <xsl:with-param name="actual_args" 
+        select="$actual_args[position()>2]"/>
+    <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
     </xsl:call-template>
    </xsl:when>
    <xsl:otherwise>
     <xsl:call-template name="get_constructor_args">
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg/target/*[1]"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
+    <xsl:with-param name="constructor_args" 
+        select="$constructor_args[position()>1]"/>
+    <xsl:with-param name="actual_args" 
+        select="$actual_args[position()>1]"/>
+    <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
     </xsl:call-template>
    </xsl:otherwise>
   </xsl:choose>
  </xsl:if>
- </xsl:when>
- <xsl:otherwise>
-  <xsl:call-template name="get_constructor_args">
-    <xsl:with-param name="no_params" select="$no_params - 1"/>
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
-    </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
+</xsl:template> 
 
 <xsl:template name="get_induction_hypothesis">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
- <xsl:if test="name($constructor_arity)='PROD'">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:if test="$constructor_args">
   <xsl:choose>
-   <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
+   <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
     <m:bvar>
      <m:ci>
-      <xsl:value-of select="$actual_arg/target/LAMBDA/target/@binder"/>
+      <xsl:value-of select="$actual_args[2]/@binder"/>
      </m:ci>
      <m:type>
       <xsl:apply-templates mode="pure" 
-           select="$actual_arg/target/LAMBDA/source"/>
+           select="$actual_args[2]/*"/>
      </m:type>
     </m:bvar>
     <xsl:call-template name="get_induction_hypothesis">
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg/target/LAMBDA/target/*[1]"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
+    <xsl:with-param name="constructor_args" 
+        select="$constructor_args[position()>1]"/>
+    <xsl:with-param name="actual_args" 
+        select="$actual_args[position()>2]"/>
+    <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
     </xsl:call-template>
    </xsl:when>
    <xsl:otherwise>
     <xsl:call-template name="get_induction_hypothesis">
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg/target/*[1]"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
+    <xsl:with-param name="constructor_args" 
+        select="$constructor_args[position()>1]"/>
+    <xsl:with-param name="actual_args" 
+        select="$actual_args[position()>1]"/>
+    <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/> 
     </xsl:call-template>
    </xsl:otherwise>
   </xsl:choose>
  </xsl:if>
- </xsl:when>
- <xsl:otherwise>
-  <xsl:call-template name="get_induction_hypothesis">
-    <xsl:with-param name="no_params" select="$no_params - 1"/>
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
-    </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
 </xsl:template>
 
 <xsl:template name="get_body">
- <xsl:param name="no_params" select="0"/>
- <xsl:param name="constructor_arity" select="/.."/>
- <xsl:param name="actual_arg" select="/.."/>
- <xsl:param name="inductive_def_name" select="''"/>
- <xsl:choose>
- <xsl:when test="$no_params = 0">
+ <xsl:param name="constructor_args" select="/.."/>
+ <xsl:param name="actual_args" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:param name="target" select="/.."/>
  <xsl:choose>
- <xsl:when test="name($constructor_arity)='PROD'">
-  <xsl:choose>
-   <xsl:when test="$constructor_arity/source//REL[@binder=$inductive_def_name]">
-    <xsl:call-template name="get_body">
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg/target/LAMBDA/target/*[1]"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
-    </xsl:call-template>
-   </xsl:when>
-   <xsl:otherwise>
-    <xsl:call-template name="get_body">
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg/target/*[1]"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
-    </xsl:call-template>
-   </xsl:otherwise>
-  </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
-  <xsl:apply-templates mode="noannot" select="$actual_arg"/>
- </xsl:otherwise> 
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
-  <xsl:call-template name="get_body">
-    <xsl:with-param name="no_params" select="$no_params - 1"/>
-    <xsl:with-param name="constructor_arity" 
-        select="$constructor_arity/target/*[1]"/>
-    <xsl:with-param name="actual_arg" 
-        select="$actual_arg"/>
-    <xsl:with-param name="inductive_def_name" 
-               select="$inductive_def_name"/>
-    </xsl:call-template>
- </xsl:otherwise>
+  <xsl:when test="$constructor_args">
+   <xsl:choose>
+    <xsl:when test="$constructor_args[1]//MUTIND[@uri=$inductive_def_uri]">
+     <xsl:call-template name="get_body">
+      <xsl:with-param name="constructor_args" 
+        select="$constructor_args[position()> 1]"/>
+      <xsl:with-param name="actual_args" 
+        select="$actual_args[position()> 2]"/>
+      <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
+      <xsl:with-param name="target" 
+               select="$target"/>
+     </xsl:call-template>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:call-template name="get_body">
+      <xsl:with-param name="constructor_args" 
+        select="$constructor_args[position()> 1]"/>
+      <xsl:with-param name="actual_args" 
+        select="$actual_args[position()> 1]"/>
+      <xsl:with-param name="inductive_def_uri" 
+               select="$inductive_def_uri"/>
+      <xsl:with-param name="target" 
+               select="$target"/>
+     </xsl:call-template>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:choose>
+    <xsl:when test="$actual_args">
+      <xsl:apply-templates select="$actual_args[1]" mode="lambda_prop"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:apply-templates mode="noannot" select="$target"/>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:otherwise> 
  </xsl:choose>
-</xsl:template>
+</xsl:template> 
 
 </xsl:stylesheet>
diff --git a/helm/style/logic.xsl b/helm/style/logic.xsl
new file mode 100644
index 000000000..0685f47b0
--- /dev/null
+++ b/helm/style/logic.xsl
@@ -0,0 +1,138 @@
+<?xml version="1.0"?>
+
+<!-- Copyright (C) 2000, HELM Team                                     -->
+<!--                                                                   -->
+<!-- This file is part of HELM, an Hypertextual, Electronic            -->
+<!-- Library of Mathematics, developed at the Computer Science         -->
+<!-- Department, University of Bologna, Italy.                         -->
+<!--                                                                   -->
+<!-- HELM is free software; you can redistribute it and/or             -->
+<!-- modify it under the terms of the GNU General Public License       -->
+<!-- as published by the Free Software Foundation; either version 2    -->
+<!-- of the License, or (at your option) any later version.            -->
+<!--                                                                   -->
+<!-- HELM is distributed in the hope that it will be useful,           -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
+<!--******************************************************************--> 
+<!-- Basic Logic                                                      -->
+<!-- (completely) Revisited: november 2002, Andrea Asperti            -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm">
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and count(child::*) = 3]">
+ <xsl:variable name="id" select="@id"/>
+ <m:apply helm:xref="{@id}">
+  <m:csymbol>false_ind</m:csymbol>
+  <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
+  <xsl:apply-templates mode="noannot" select="*[3]"/>
+ </m:apply>
+</xsl:template>
+
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/and_ind.con'] and 
+ count(child::*) = 6 and name(*[5])='LAMBDA' and 
+ count(*[5]/decl) = 2]">
+  <xsl:variable name="id" select="@id"/>
+  <m:apply helm:xref="{@id}">
+   <m:csymbol>and_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]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+   <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+   <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+   <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
+   <xsl:apply-templates mode="noannot" select="*[5]/target/*"/> 
+  </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/or_ind.con'] 
+ and count(child::*) = 7 and 
+ name(*[5])='LAMBDA' and count(*[5]/decl) = 1 and 
+ name(*[6])='LAMBDA' and count(*[6]/decl) = 1 ]">
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="definition_url" 
+   select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
+ <m:apply helm:xref="{@id}">
+  <m:csymbol>full_or_ind</m:csymbol>
+  <xsl:apply-templates mode="noannot" select="*[7]"/>
+  <xsl:for-each select="$InnerTypes">
+   <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+  </xsl:for-each>
+  <m:apply>
+   <m:csymbol>left_case</m:csymbol>
+   <m:bvar>
+    <m:ci>
+     <xsl:value-of select="*[5]/*[1]/@binder"/>
+    </m:ci>
+    <m:type>
+     <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+    </m:type>
+   </m:bvar>
+   <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
+  </m:apply>
+  <m:apply>
+   <m:csymbol>right_case</m:csymbol>
+   <m:bvar>
+    <m:ci>
+     <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
+    </m:ci>
+    <m:type>
+     <xsl:apply-templates mode="pure" select="*[6]/*[1]/*"/>
+    </m:type>
+   </m:bvar>
+   <xsl:apply-templates mode="noannot" select="*[6]/target"/>
+  </m:apply>
+ </m:apply>
+
+<!-- da tertminare 
+  </xsl:when>
+  <xsl:otherwise>
+   <m:apply helm:xref="{@id}">
+    <m:csymbol>or_ind</m:csymbol>
+    <xsl:apply-templates mode="noannot" select="*[7]"/>
+    <xsl:for-each select="$InnerTypes">
+     <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
+    </xsl:for-each> 
+    <xsl:apply-templates mode="pure" select="*[5]"/>
+    <xsl:apply-templates mode="pure" select="*[6]"/>
+   </m:apply>
+  </xsl:otherwise>
+ </xsl:choose>
+-->
+</xsl:template> 
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'] and
+ count(child::*) = 6 and
+ name(*[5])='LAMBDA' and count(*[5]/decl) = 2 ]">
+  <xsl:variable name="id" select="@id"/>
+   <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]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+    <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
+    <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+    <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
+    <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
+   </m:apply>
+</xsl:template>
+
+</xsl:stylesheet>
+
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index 405529785..372ae22c1 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -119,6 +119,8 @@
 </xsl:template>
 
 <xsl:template match="ConstantType" mode="noannot">
+    <xsl:variable name="ConstantBodyUrl" 
+                  select="concat($BaseCICURI,'.body')"/>
     <Definition name="{@name}" helm:xref="{@id}">  
      <xsl:if test="string(@params) != &quot;&quot;">
       <Params>
@@ -139,7 +141,9 @@
        </body>
       </xsl:otherwise>
      </xsl:choose> -->
-     <body/>
+     <body>
+      <m:ci definitionURL="{$ConstantBodyUrl}">click here</m:ci>
+     </body>
      <type>
        <xsl:apply-templates select="./*[1]"/>
      </type>
diff --git a/helm/style/params.xsl b/helm/style/params.xsl
index 3d16f62e2..355baef56 100644
--- a/helm/style/params.xsl
+++ b/helm/style/params.xsl
@@ -39,16 +39,18 @@
 <!-- CSC: PROBLEMA: URI CHE NON CONTENGONO / ED INIZIANO CON cic: -->
 <xsl:template name="name_of_uri">
  <xsl:param name="uri" select="&quot;&quot;"/>
+ <xsl:param name="extension" select="'.con'"/>
  <xsl:variable name="suffix" select="substring-after($uri, &quot;/&quot;)"/>
  <xsl:choose>
   <xsl:when test="$suffix = &quot;&quot;">
    <!-- CSC: PROBLEMA: .con PUO' APPARIRE ALL'INTERNO DELLE URI ===>
      SCRIVERE UNA FUNZIONE RICORSIVA CHE RISOLVA -->
-   <xsl:value-of select="substring-before($uri,&quot;.con&quot;)"/>
+   <xsl:value-of select="substring-before($uri,$extension)"/>
   </xsl:when>
   <xsl:otherwise>
    <xsl:call-template name="name_of_uri">
     <xsl:with-param name="uri" select="$suffix"/>
+    <xsl:with-param name="extension" select="$extension"/> 
    </xsl:call-template>
   </xsl:otherwise>
  </xsl:choose>
@@ -98,6 +100,25 @@
  </xsl:choose>   
 </xsl:template>
 
+<!-- path gives the path of a uri, up to the final name -->
+<xsl:template name="path">
+ <xsl:param name="uri" select="&quot;&quot;"/>
+ <xsl:param name="current_path" select="&quot;&quot;"/>
+ <xsl:choose>
+  <xsl:when test="(substring-after($uri,&quot;/&quot;) != &quot;&quot;)">
+   <xsl:call-template name="path">
+    <xsl:with-param 
+        name="uri" select="substring-after($uri,&quot;/&quot;)"/>
+    <xsl:with-param
+        name="current_path" select="concat($current_path,substring-before($uri,&quot;/&quot;),'/')"/> 
+   </xsl:call-template>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:value-of select="$current_path"/>
+  </xsl:otherwise>
+ </xsl:choose>   
+</xsl:template>
+
 <xsl:template name="blank_counting">
  <xsl:param name="string" select="&quot;&quot;"/>
  <xsl:param name="counter" select="0"/>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 86ad8292e..78efb9cb1 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -34,6 +34,11 @@
                               xmlns:m="http://www.w3.org/1998/Math/MathML"
                               xmlns:helm="http://www.cs.unibo.it/helm">
 
+<xsl:include href="logic.xsl"/>
+<xsl:include href="inductive.xsl"/>
+<xsl:include href="rewrite.xsl"/>
+<xsl:include href="diseq.xsl"/>
+
 <!-- ************************* LOGIC *********************************-->
 
 <!-- Proof objects -->
@@ -76,9 +81,20 @@
 
 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
 
-<!-- LAMBDA has inner type only if it is not nested inside another lambda -->
 <xsl:template match="LAMBDA" mode="noannot">
- <xsl:variable name="id" select="decl/@id"/>
+ <xsl:choose>
+  <xsl:when test="@sort='Prop'">
+   <xsl:apply-templates select="*[1]" mode="lambda_prop"/>
+  </xsl:when>
+  <xsl:otherwise>
+   <!-- mode lambda is defined in content.xsl -->
+   <xsl:apply-templates select="*[1]" mode="lambda"/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="decl" mode="lambda_prop">
+ <xsl:variable name="id" select="@id"/>
  <xsl:variable name="innertype_available">
   <xsl:for-each select="$InnerTypes">
    <xsl:if test="key('typeid',$id)/*">
@@ -86,257 +102,132 @@
    </xsl:if>
   </xsl:for-each>
  </xsl:variable>
- <!--xsl:value-of select="concat('NL: ',$naturalLanguage,'  IA:  ',$innertype_available)"/-->
  <xsl:choose>
-  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
-   <m:apply helm:xref="{decl/@id}">
+  <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
+   <m:apply helm:xref="{@id}">
     <m:csymbol>proof</m:csymbol>
-    <xsl:apply-templates mode="proof_transform" select="."/>
+    <m:lambda helm:xref="{@id}">
+     <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:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
+    </m:lambda>
     <xsl:for-each select="$InnerTypes">
      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
     </xsl:for-each>
    </m:apply>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:apply-templates select="." mode="pure"/>
+   <m:lambda helm:xref="{@id}">
+    <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:apply-templates select="following-sibling::*[1]" mode="lambda_prop"/>
+   </m:lambda>
   </xsl:otherwise>
  </xsl:choose>
 </xsl:template>
 
-<!-- ALL these elements have inner type -->
-<xsl:template match="LETIN|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="target" mode="lambda_prop">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+<!-- LETIN -->
+
+<xsl:template match="LETIN" mode="noannot">
+ <xsl:choose>
+  <xsl:when test="@sort='Prop'">
+   <xsl:apply-templates select="*[1]" mode="letin_prop"/>
+  </xsl:when>
+  <xsl:otherwise>
+   <!-- mode letin is defined in content.xsl -->
+   <xsl:apply-templates select="*[1]" mode="letin_pure"/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<xsl:template match="def" mode="letin_prop">
  <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+  <xsl:for-each select="$InnerTypes">
+   <xsl:if test="key('typeid',$id)/*">
+    <xsl:text>yes</xsl:text>
+   </xsl:if>
+  </xsl:for-each>
+ </xsl:variable>
  <xsl:choose>
-  <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
+  <xsl:when test="$naturalLanguage='yes' and $innertype_available='yes'">
    <m:apply helm:xref="{@id}">
     <m:csymbol>proof</m:csymbol>
-    <xsl:apply-templates mode="proof_transform" select="."/>
+    <m:apply helm:xref="{@id}">
+     <m:csymbol>let_in</m:csymbol>
+     <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:bvar>
+     <xsl:apply-templates select="*[1]" mode="noannot"/>
+     <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
+    </m:apply>
     <xsl:for-each select="$InnerTypes">
      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
     </xsl:for-each>
    </m:apply>
   </xsl:when>
   <xsl:otherwise>
-   <xsl:choose>
-    <xsl:when test="name()='APPLY'">
-     <!-- This is the case of an applicative expression wich is not
-          a proof but could contains proofs...
-          MODE LETIN OR MODE PURE ??? Big question -->
-     <xsl:apply-templates select="." mode="pure"/>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:apply-templates select="." mode="pure"/>
-    </xsl:otherwise>
-   </xsl:choose>
+   <m:apply helm:xref="{@id}">
+    <m:csymbol>let_in</m:csymbol>
+    <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:bvar>
+    <xsl:apply-templates select="*[1]" mode="noannot"/>
+    <xsl:apply-templates select="following-sibling::*[1]" mode="letin_prop"/>
+   </m:apply>
   </xsl:otherwise>
  </xsl:choose>
 </xsl:template>
 
-<!-- si presuppone che il tipo induttivo non sia mutuamente 
-     induttivo. Bisognerebbe andare a vedere l'ultimo parametro
-     del presunto "principio di induzione", tirare fuori il tipo induttivo
-     e vedere se il suo nome coincide con il prefisso di _ind. 
-     Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
-     parametro di nat_double_ind e' di tipo nat, e nat e' diverso
-     da nat_double. Per ora, verifico solo l'esistenza di nat_double,
-     ma questo, benche' non porti ad errore, non copre tutti i
-     casi per quelli mutuamente induttivi -->
-
-<xsl:template mode="try_inductive" match="APPLY">
-   <xsl:variable name="id" select="@id"/>
-   <xsl:choose>
-    <xsl:when test="CONST[1]">
-     <xsl:variable name="uri" select="CONST[1]/@uri"/>
-     <xsl:choose>
-      <xsl:when test="contains($uri,'_ind.con')">
-       <xsl:variable name="ind_uri" 
-         select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
-       <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
-       <xsl:variable name="inductive_def" 
-     select="document($InductiveTypeUrl)/InductiveDefinition"/>
-       <!-- check if the corresponding inductive definition actually
-            exists -->
-       <xsl:choose>
-        <xsl:when test="$inductive_def">
-         <xsl:variable name="ind_name">
-          <xsl:call-template name="get_name">
-           <xsl:with-param name="uri" select="$uri"/>
-          </xsl:call-template>
-         </xsl:variable>
-         <xsl:variable name="no_params">
-          <xsl:call-template name="get_no_params">
-           <xsl:with-param name="first_uri" select="$CICURI"/>
-           <xsl:with-param name="second_uri" select="$uri"/>
-          </xsl:call-template>
-         </xsl:variable>
-         <xsl:apply-templates mode="inductive" select=".">
-          <xsl:with-param name="inductive_def_uri" 
-           select="$ind_uri"/>
-          <xsl:with-param name="inductive_def" 
-           select="$inductive_def"/>
-          <xsl:with-param name="section_params" select="$no_params"/>
-          <xsl:with-param name="inductive_def_index" select="1"/>
-          <xsl:with-param name="inductive_def_name" select="$ind_name"/>
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:otherwise>
-         <xsl:apply-templates mode="letin" select="."/>
-        </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-      <xsl:otherwise>
-       <xsl:apply-templates mode="letin" select="."/>
-      </xsl:otherwise>
-     </xsl:choose>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:apply-templates mode="letin" select="."/>
-    </xsl:otherwise>
-   </xsl:choose>
+<xsl:template match="target" mode="letin_prop">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
 </xsl:template>
 
-<xsl:template mode="eq_transitive" match="*">
- <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
+<!-- ALL these elements have inner type -->
+<xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
+ <xsl:variable name="id" select="@id"/>
  <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/algebra/CSetoids/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 test="$naturalLanguage='yes' and @sort='Prop'">
+   <m:apply helm:xref="{@id}">
+    <m:csymbol>proof</m:csymbol>
+    <xsl:apply-templates mode="proof_transform" select="."/>
+    <xsl:for-each select="$InnerTypes">
+     <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
+    </xsl:for-each>
+   </m:apply>
   </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>
-
-<xsl:template mode="diseq" match="*">
-  <xsl:param name="rel" select="'eq'"/>
-  <xsl:choose>
-  <xsl:when test="name()='APPLY'">
-      <xsl:variable name="id" select="@id"/>
    <xsl:choose>
-    <!-- ricordarsi di trattare il parametro -->
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_transitive.con'] and count(child::*) = 7">
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-    </xsl:when> 
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdl.con'] and count(child::*) = 7">
-       <m:eq/>
-       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
-       <xsl:call-template name="generate_side_proof">
-        <xsl:with-param name="proof" select="*[7]"/>
-        <xsl:with-param name="show_statement" select="0"/>
-       </xsl:call-template>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-    </xsl:when> 
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algerba/COrdFields/leEq_less_trans.con'] and count(child::*) = 7">
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
+    <xsl:when test="name()='APPLY'">
+     <!-- This is the case of an applicative expression wich is not
+          a proof but could contains proofs...
+          MODE LETIN OR MODE PURE ??? Big question -->
+     <xsl:apply-templates select="." mode="pure"/>
     </xsl:when>
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_leEq_trans.con'] and count(child::*) = 7">
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-    </xsl:when>  
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdr.con'] and count(child::*) = 7">
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'eq'"/>
-       </xsl:apply-templates>
-    </xsl:when>  
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_transitive_unfolded.con'] and count(child::*) = 7">
-      <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-     </xsl:when> 
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdr.con'] and count(child::*) = 7">
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'eq'"/>
-       </xsl:apply-templates>
-     </xsl:when>
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdl.con'] and count(child::*) = 7">
-       <m:eq/>
-       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
-       <xsl:call-template name="generate_side_proof">
-        <xsl:with-param name="proof" select="*[7]"/>
-        <xsl:with-param name="show_statement" select="0"/>
-       </xsl:call-template>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-    </xsl:when> 
-    <!-- 
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
-     <xsl:apply-templates mode="diseq" select="*[6]"/>
-     <m:eq/>
-     <xsl:apply-templates mode="noannot" select="*[4]"/>
-     <m:eq/>
-     <xsl:apply-templates mode="diseq" select="*[7]"/>
-    </xsl:when> 
-    -->
     <xsl:otherwise>
-     <xsl:element name="{concat('m:',$rel)}"/>
-     <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->  
-     <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:apply-templates select="." mode="pure"/>
     </xsl:otherwise>
    </xsl:choose>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:element name="{concat('m:',$rel)}"/> 
-   <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> --> 
-   <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>
@@ -346,363 +237,16 @@
   <xsl:when test="name()='APPLY'">
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
-    <!-- Algebra equality (eq_transitive_unfolded) -->
-    <!-- It requires a special mode "eq_transitive"-->
-    <!-- togliere il parametro -->
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/eq_transitive_unfolded.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>eq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-     </m:apply>
-    </xsl:when>
-    <!-- Algebra disequalities -->
-    <!-- It requires a special mode "diseq"-->
-    <!-- togliere il parametro -->
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_transitive.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-     </m:apply>
-    </xsl:when> 
-     <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdl.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-       <m:eq/>
-       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
-       <xsl:call-template name="generate_side_proof">
-        <xsl:with-param name="proof" select="*[7]"/>
-        <xsl:with-param name="show_statement" select="0"/>
-       </xsl:call-template>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-     </m:apply>
-    </xsl:when>
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_less_trans.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-     </m:apply>
-    </xsl:when> 
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_leEq_trans.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-     </m:apply>
-    </xsl:when>  
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdr.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'leq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'eq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-     </m:apply>
-    </xsl:when>  
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_transitive_unfolded.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-     </m:apply>
-    </xsl:when>  
-    <!-- togliere il parametro -->
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdr.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-       <xsl:apply-templates mode="diseq" select="*[7]">
-        <xsl:with-param name="rel" select="'eq'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-     </m:apply>
-    </xsl:when>
-    <!-- togliere il parametro -->
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdl.con'] and count(child::*) = 7">
-     <m:apply>
-       <m:csymbol>diseq_chain</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-       <m:eq/>
-       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
-       <xsl:call-template name="generate_side_proof">
-        <xsl:with-param name="proof" select="*[7]"/>
-        <xsl:with-param name="show_statement" select="0"/>
-       </xsl:call-template>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-       <xsl:apply-templates mode="diseq" select="*[6]">
-        <xsl:with-param name="rel" select="'lt'"/>
-       </xsl:apply-templates>
-       <xsl:apply-templates mode="noannot" select="*[4]"/>
-     </m:apply>
-    </xsl:when> 
-    <!-- EQUALITY -->
-    <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
-      <m:apply>
-       <m:csymbol>rw_step</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[5]"/>
-       <xsl:apply-templates mode="pure" select="*[3]"/>
-       <xsl:apply-templates mode="pure" select="*[6]"/>
-       <xsl:call-template name="generate_side_proof">
-        <xsl:with-param name="proof" select="*[7]"/>
-       </xsl:call-template>
-       <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
-      </m:apply>
-    </xsl:when>
-    <!-- EQUALITY with extra-parameters -->
-    <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
- attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
-      <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>      
-      <xsl:choose>
-       <xsl:when test="$no_extraproofs=0"> 
-        <m:apply>
-         <m:csymbol>rewrite_and_apply</m:csymbol>
-         <m:apply>
-          <m:csymbol>rw_step</m:csymbol>
-          <xsl:apply-templates mode="noannot" select="*[5]"/>
-          <xsl:apply-templates mode="pure" select="*[3]"/>
-          <xsl:apply-templates mode="pure" select="*[6]"/>
-          <xsl:call-template name="generate_side_proof">
-           <xsl:with-param name="proof" select="*[7]"/>
-           </xsl:call-template>
-          <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
-         </m:apply>
-         <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
-        </m:apply>
-       </xsl:when>
-       <xsl:otherwise>
-        <xsl:choose>
-         <xsl:when test="*[5]/@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" select="'h1'"/>
-             </xsl:call-template>
-            </m:ci>
-            <xsl:apply-templates mode="noannot" select="*[5]"/>
-           </m:apply>
-           <xsl:call-template name="gen_let">
-            <xsl:with-param name="init_pos" select="1"/>
-            <xsl:with-param name="from" select="7"/>
-           </xsl:call-template>
-           <m:apply>
-            <m:csymbol>rewrite_and_apply</m:csymbol>
-            <m:apply>
-             <m:csymbol>rw_step</m:csymbol>
-             <m:ci>
-              <xsl:call-template name="insert_subscript">
-               <xsl:with-param name="node_value" select="'h1'"/>
-              </xsl:call-template>
-             </m:ci>
-             <xsl:apply-templates mode="pure" select="*[3]"/>
-             <xsl:apply-templates mode="pure" select="*[6]"/>
-             <xsl:call-template name="generate_side_proof">
-              <xsl:with-param name="proof" select="*[7]"/>
-             </xsl:call-template>
-             <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
-            </m:apply>
-            <xsl:apply-templates mode="flat" select="*[8]">
-             <xsl:with-param name="n">
-              <xsl:value-of select="2"/>
-             </xsl:with-param>
-            </xsl:apply-templates>
-           </m:apply>
-          </m:apply>
-         </xsl:when>
-         <xsl:otherwise>
-          <m:apply helm:xref="{@id}">
-           <m:csymbol>letin</m:csymbol>
-           <xsl:call-template name="gen_let">
-            <xsl:with-param name="init_pos" select="0"/>
-            <xsl:with-param name="form" select="7"/>
-           </xsl:call-template>
-           <m:apply>
-            <m:csymbol>rewrite_and_apply</m:csymbol>
-            <m:apply>
-             <m:csymbol>rw_step</m:csymbol>
-             <xsl:apply-templates mode="pure" select="*[5]"/>
-             <xsl:apply-templates mode="pure" select="*[3]"/>
-             <xsl:apply-templates mode="pure" select="*[6]"/>             
-             <xsl:call-template name="generate_side_proof">
-              <xsl:with-param name="proof" select="*[7]"/>
-             </xsl:call-template>
-             <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
-            </m:apply>
-            <xsl:apply-templates mode="flat" select="*[8]">
-             <xsl:with-param name="n">
-              <xsl:value-of select="1"/>
-             </xsl:with-param>
-            </xsl:apply-templates>
-           </m:apply>
-          </m:apply>
-         </xsl:otherwise>
-        </xsl:choose>
-       </xsl:otherwise>
-      </xsl:choose>
-    </xsl:when>
-    <!-- False_ind -->
-    <xsl:when test="CONST[
-     attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and 
-     count(child::*) = 3">
-     <m:apply helm:xref="{@id}">
-       <m:csymbol>false_ind</m:csymbol>
-       <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
-       <xsl:apply-templates mode="noannot" select="*[3]"/>
-     </m:apply>
-    </xsl:when>
-    <!-- gestire meglio il caso di and_ind quando la prova 
-         non e' della forma \x.\y.M -->
-    <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/and_ind.con'] 
- and count(child::*) = 6 
- and name(*[5])='LAMBDA'"> 
-      <m:apply helm:xref="{@id}">
-       <m:csymbol>and_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]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
-       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
-       <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/> 
-      </m:apply>
-    </xsl:when>
-    <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/or_ind.con'] 
- and count(child::*) = 7">
-      <xsl:choose>
-       <xsl:when test="name(*[5])='LAMBDA' 
-                 and name(*[6])='LAMBDA'">
-        <xsl:variable name="definition_url" 
-            select="'cic:/Coq/Init/Logic/or.ind'"/>
-        <m:apply helm:xref="{@id}">
-         <m:csymbol>full_or_ind</m:csymbol>
-         <xsl:apply-templates mode="noannot" select="*[7]"/>
-         <xsl:for-each select="$InnerTypes">
-          <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
-         </xsl:for-each>
-         <m:apply>
-          <m:csymbol>left_case</m:csymbol>
-          <m:bvar>
-           <m:ci>
-            <xsl:value-of select="*[5]/*[1]/@binder"/>
-           </m:ci>
-           <m:type>
-            <xsl:apply-templates mode="pure" select="*[5]/*[1]/*[1]"/>
-           </m:type>
-          </m:bvar>
-          <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
-         </m:apply>
-         <m:apply>
-          <m:csymbol>right_case</m:csymbol>
-          <m:bvar>
-           <m:ci>
-            <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
-           </m:ci>
-           <m:type>
-            <xsl:apply-templates mode="pure" select="*[6]/*[1]/*[1]"/>
-           </m:type>
-          </m:bvar>
-          <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
-         </m:apply>
-        </m:apply>
-       </xsl:when>
-       <xsl:otherwise>
-        <m:apply helm:xref="{@id}">
-         <m:csymbol>or_ind</m:csymbol>
-         <xsl:apply-templates mode="noannot" select="*[7]"/>
-         <xsl:for-each select="$InnerTypes">
-          <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
-         </xsl:for-each>
-         <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/ex_ind.con'])  
- and count(child::*) = 6 
- and name(*[5])='LAMBDA' 
- and name(*[5]/*[2])='decl'"> 
-      <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]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
-       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
-       <xsl:apply-templates mode="proof_transform" select="*[5]/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'">
+    <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2">
+    <!-- old
+         and *[2]/@sort='Prop'"> -->
      <m:apply helm:xref="{@id}">
-      <m:csymbol>letin</m:csymbol>
-      <m:apply>
-       <m:csymbol>let</m:csymbol>
+      <m:csymbol>let_in</m:csymbol>
+      <m:bvar>
        <m:ci>
         <xsl:call-template name="insert_subscript">
          <xsl:with-param name="node_value">
@@ -710,8 +254,8 @@
          </xsl:with-param>
         </xsl:call-template>
        </m:ci>
-       <xsl:apply-templates mode="noannot" select="*[2]"/>
-      </m:apply>
+      </m:bvar>
+      <xsl:apply-templates mode="noannot" select="*[2]"/>
       <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
      </m:apply>
     </xsl:when>
@@ -720,32 +264,6 @@
     </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>
-     </xsl:when>
-     <xsl:otherwise>
-      <xsl:apply-templates mode="pure" select="."/>
-     </xsl:otherwise>
-    </xsl:choose>
-   </xsl:when>
   <xsl:otherwise>
    <xsl:apply-templates select="." mode="pure"/>
   </xsl:otherwise>
@@ -875,6 +393,50 @@
    </xsl:choose>
 </xsl:template>
 
+
+<xsl:template name="gen_let">
+ <xsl:param name="init_pos" select="1"/>
+ <xsl:param name="from" select="0"/>
+  <xsl:apply-templates mode="gen_let_aux" select="*[position() = ($from+1)]">
+   <xsl:with-param name="init_pos" select="$init_pos"/>
+  </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template mode="gen_let_aux" match="*">
+ <xsl:param name="init_pos" select="1"/>
+ <xsl:variable name="id" select="@id"/>
+ <xsl:variable name="innertype_available">
+  <xsl:for-each select="$InnerTypes">
+   <xsl:if test="key('typeid',$id)/*">
+    <xsl:text>yes</xsl:text>
+   </xsl:if>
+  </xsl:for-each>
+ </xsl:variable>
+ <xsl:choose>
+  <xsl:when test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
+   <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="concat('h',$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
+    <xsl:apply-templates mode="noannot" select="."/>
+   </m:apply>
+   <xsl:if test="following-sibling::*[1]">
+    <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
+     <xsl:with-param name="init_pos" select="$init_pos+1"/>
+    </xsl:apply-templates>
+   </xsl:if>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:if test="following-sibling::*[1]">
+    <xsl:apply-templates mode="gen_let_aux" select="following-sibling::*[1]">
+     <xsl:with-param name="init_pos" select="$init_pos"/>
+    </xsl:apply-templates>
+   </xsl:if>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- questa vecchia versione (di Claudio??) sembra bacata come un melone.
+
 <xsl:template name="gen_let">
  <xsl:param name="init_pos" select="0"/>
  <xsl:param name="from" select="0"/>
@@ -895,11 +457,12 @@
         </m:apply>
        </xsl:if>
       </xsl:for-each>
-</xsl:template>
+</xsl:template> -->
 
 <xsl:template match="*" mode="erase">
   <xsl:choose>
-   <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+   <xsl:when test="@sort='Prop' 
+                   or name()='instantiate' or $naturalLanguage='no'">
     <xsl:apply-templates mode="pure" select="."/>
    </xsl:when>
    <xsl:otherwise>
@@ -925,7 +488,8 @@
   <xsl:otherwise>
    <!-- forse bisognerebbe trattare solo l'elemento di testa -->
    <xsl:choose>
-   <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+   <xsl:when test="@sort='Prop' 
+                   or name()='instantiate' or $naturalLanguage='no'">
     <xsl:apply-templates mode="pure" select="."/>
    </xsl:when>
    <xsl:otherwise>
@@ -959,7 +523,7 @@
   </xsl:when>
   <xsl:otherwise>
    <xsl:choose>
-    <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
+    <xsl:when test="name()='REL' or name()='instantiate' or @sort='Prop' or $naturalLanguage='no'">
      <xsl:apply-templates mode="pure" select="."/>
     </xsl:when>
     <xsl:otherwise>
@@ -992,27 +556,5 @@
  </xsl:choose>
 </xsl:template>
 
-<!-- <xsl:template match="APPLY[CONST[
- attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
-    <xsl:choose>
-     <xsl:when test="count(child::*) > 4">
-      <m:apply helm:xref="{@id}">
-       <m:csymbol>app</m:csymbol>
-       <xsl:apply-templates mode="pure" select="*[1]"/>
-       <m:ci>*</m:ci>
-       <m:ci>*</m:ci>
-       <m:ci>*</m:ci>
-       <xsl:apply-templates mode="flat" select="*[5]"/>
-      </m:apply>
-     </xsl:when>
-     <xsl:otherwise>
-      <m:apply helm:xref="{@id}">
-       <m:csymbol>app</m:csymbol>
-       <xsl:apply-templates mode="flat" select="*[1]"/>
-      </m:apply>
-     </xsl:otherwise>
-    </xsl:choose>
-</xsl:template>  -->
-
 
 </xsl:stylesheet>
diff --git a/helm/style/rewrite.xsl b/helm/style/rewrite.xsl
new file mode 100644
index 000000000..e361944d3
--- /dev/null
+++ b/helm/style/rewrite.xsl
@@ -0,0 +1,135 @@
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
+<!-- GNU General Public License for more details.                      -->
+<!--                                                                   -->
+<!-- You should have received a copy of the GNU General Public License -->
+<!-- along with HELM; if not, write to the Free Software               -->
+<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
+<!-- MA  02111-1307, USA.                                              -->
+<!--                                                                   -->
+<!-- For details, see the HELM World-Wide-Web page,                    -->
+<!-- http://cs.unibo.it/helm/.                                         -->
+
+<!--******************************************************************--> 
+<!-- Basic Logic                                                      -->
+<!-- (completely) Revisited: february 2001, Andrea Asperti            -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
+<!--******************************************************************-->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML"
+                              xmlns:helm="http://www.cs.unibo.it/helm">
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7]">
+ <xsl:variable name="id" select="@id"/>
+  <m:apply>
+   <m:csymbol>rw_step</m:csymbol>
+   <xsl:apply-templates mode="noannot" select="*[5]"/>
+   <xsl:apply-templates mode="pure" select="*[3]"/>
+   <xsl:apply-templates mode="pure" select="*[6]"/>
+   <xsl:call-template name="generate_side_proof">
+    <xsl:with-param name="proof" select="*[7]"/>
+   </xsl:call-template>
+  </m:apply>
+</xsl:template>
+
+<xsl:template mode="proof_transform" match="APPLY[CONST[
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7]">
+ <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>      
+ <xsl:choose>
+  <xsl:when test="$no_extraproofs=0"> 
+   <m:apply>
+    <m:csymbol>rewrite_and_apply</m:csymbol>
+    <m:apply>
+     <m:csymbol>rw_step</m:csymbol>
+     <xsl:apply-templates mode="noannot" select="*[5]"/>
+     <xsl:apply-templates mode="pure" select="*[3]"/>
+     <xsl:apply-templates mode="pure" select="*[6]"/>
+     <xsl:call-template name="generate_side_proof">
+      <xsl:with-param name="proof" select="*[7]"/>
+     </xsl:call-template>
+    </m:apply>
+    <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
+   </m:apply>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:choose>
+    <xsl:when test="*[5]/@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" select="'h1'"/>
+        </xsl:call-template>
+       </m:ci>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+      </m:apply>
+      <xsl:call-template name="gen_let">
+       <xsl:with-param name="init_pos" select="1"/>
+       <xsl:with-param name="from" select="7"/>
+      </xsl:call-template>
+      <m:apply>
+       <m:csymbol>rewrite_and_apply</m:csymbol>
+       <m:apply>
+        <m:csymbol>rw_step</m:csymbol>
+        <m:ci>
+         <xsl:call-template name="insert_subscript">
+          <xsl:with-param name="node_value" select="'h1'"/>
+         </xsl:call-template>
+        </m:ci>
+        <xsl:apply-templates mode="pure" select="*[3]"/>
+        <xsl:apply-templates mode="pure" select="*[6]"/>
+        <xsl:call-template name="generate_side_proof">
+         <xsl:with-param name="proof" select="*[7]"/>
+        </xsl:call-template>
+       </m:apply>
+       <xsl:apply-templates mode="flat" select="*[8]">
+        <xsl:with-param name="n">
+         <xsl:value-of select="2"/>
+        </xsl:with-param>
+       </xsl:apply-templates>
+      </m:apply>
+     </m:apply>
+    </xsl:when>
+    <xsl:otherwise>
+     <m:apply helm:xref="{@id}">
+      <m:csymbol>letin</m:csymbol>
+      <xsl:call-template name="gen_let">
+       <xsl:with-param name="init_pos" select="0"/>
+       <xsl:with-param name="form" select="7"/>
+      </xsl:call-template>
+      <m:apply>
+       <m:csymbol>rewrite_and_apply</m:csymbol>
+       <m:apply>
+        <m:csymbol>rw_step</m:csymbol>
+        <xsl:apply-templates mode="pure" select="*[5]"/>
+        <xsl:apply-templates mode="pure" select="*[3]"/>
+        <xsl:apply-templates mode="pure" select="*[6]"/>             
+        <xsl:call-template name="generate_side_proof">
+         <xsl:with-param name="proof" select="*[7]"/>
+        </xsl:call-template>
+       </m:apply>
+       <xsl:apply-templates mode="flat" select="*[8]">
+        <xsl:with-param name="n">
+         <xsl:value-of select="1"/>
+        </xsl:with-param>
+       </xsl:apply-templates>
+      </m:apply>
+     </m:apply>
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+</xsl:stylesheet>
\ No newline at end of file
diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl
index 1acaf5a78..5d2eb2e4c 100644
--- a/helm/style/rootcontent.xsl
+++ b/helm/style/rootcontent.xsl
@@ -74,6 +74,7 @@
 <xsl:variable name="ConstantTypeUrl"><xsl:call-template name="makeURL4InnerTypes"><xsl:with-param name="uri" select="$BaseCICURI"/></xsl:call-template></xsl:variable>
 <xsl:variable name="AnnotationsUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$AnnotationsUri"/></xsl:call-template></xsl:variable>
 
+
 <!-- WARNING: Using lazy evaluation: $CICURI.* may not exist, but -->
 <!-- document() is called only by need!!!                         -->
 <xsl:variable name="InnerTypes" select="document($InnerTypesUrl)"/> 
@@ -81,6 +82,13 @@
 
 <xsl:include href="headercontent.xsl"/>
 <xsl:include href="proofs.xsl"/>
-<xsl:include href="inductive.xsl"/>
 <xsl:variable name="showproof" select="0"/>
 </xsl:stylesheet>
+
+
+
+
+
+
+
+
diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt
index 2f31b969a..9b3260cbf 100644
--- a/helm/style/xslt_index.txt
+++ b/helm/style/xslt_index.txt
@@ -3,6 +3,7 @@ annotatedpres.xsl
 content.xsl
 content_to_html.xsl
 contentlib.xsl
+diseq.xsl
 drop_coercions.xsl
 expandobj.xsl
 genmmlid.xsl
@@ -15,6 +16,7 @@ inductive.xsl
 lambda.xsl
 link.xsl
 links_library.xsl
+logic.xsl
 mk_dep_graph.xsl
 mk_meta_and_dep_graph.xsl
 mk_meta_graph.xsl
@@ -27,6 +29,7 @@ objcontent.xsl
 objtheorycontent.xsl
 params.xsl
 proofs.xsl
+rewrite.xsl
 ricerca.xsl
 ring.xsl
 rootcontent.xsl
-- 
2.39.2