From 5f2de2d1d6c8520e39c1c3793a4c2776dcf7c7c1 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Jan 2004 15:13:45 +0000
Subject: [PATCH] Branch V7_3_new_exportation merged.

---
 helm/meta_style/.cvsignore           |   1 +
 helm/meta_style/Makefile             |  19 +-
 helm/meta_style/algebra.xml          |  43 +-
 helm/meta_style/arith.xml            |   8 +-
 helm/meta_style/basic.xml            |  23 +-
 helm/meta_style/list.xml             |  60 ++
 helm/meta_style/meta_cic2mathml.xsl  | 245 ++++----
 helm/meta_style/positive.xsl         |  57 +-
 helm/meta_style/set.xml              | 205 +++----
 helm/meta_style/xslt_index.txt       |   1 +
 helm/style/annotatedcont.xsl         |   6 +-
 helm/style/content.xsl               | 152 +++--
 helm/style/content_to_html.xsl       | 176 +++++-
 helm/style/diseq.xsl                 | 336 +++++++++++
 helm/style/drop_coercions.xsl        |  22 +-
 helm/style/headercontent.xsl         |  10 +-
 helm/style/html_init.xsl             |   2 -
 helm/style/inductive.xsl             | 369 +++++++------
 helm/style/ite.xsl                   |  48 ++
 helm/style/link.xsl                  |  11 +-
 helm/style/logic.xsl                 | 155 ++++++
 helm/style/mk_meta_and_dep_graph.xsl |  20 +-
 helm/style/mk_meta_theory.xsl        |  58 +-
 helm/style/mmlctop.xsl               |  44 +-
 helm/style/mmlextension.xsl          | 257 ++++++++-
 helm/style/mmlnotation.xsl           |  34 +-
 helm/style/objcontent.xsl            |  77 ++-
 helm/style/objtheorycontent.xsl      |  22 +-
 helm/style/params.xsl                | 116 +++-
 helm/style/proofs.xsl                | 798 ++++++---------------------
 helm/style/rewrite.xsl               | 135 +++++
 helm/style/ring.xsl                  |  72 +--
 helm/style/xslt_index.txt            |   4 +
 33 files changed, 2265 insertions(+), 1321 deletions(-)
 create mode 100644 helm/meta_style/list.xml
 create mode 100644 helm/style/diseq.xsl
 create mode 100644 helm/style/ite.xsl
 create mode 100644 helm/style/logic.xsl
 create mode 100644 helm/style/rewrite.xsl

diff --git a/helm/meta_style/.cvsignore b/helm/meta_style/.cvsignore
index b88948804..b20cfb281 100644
--- a/helm/meta_style/.cvsignore
+++ b/helm/meta_style/.cvsignore
@@ -3,3 +3,4 @@ arith.xsl
 basic.xsl
 reals.xsl
 set.xsl
+list.xsl
diff --git a/helm/meta_style/Makefile b/helm/meta_style/Makefile
index c0e5fc645..f51cc8094 100644
--- a/helm/meta_style/Makefile
+++ b/helm/meta_style/Makefile
@@ -1,14 +1,14 @@
 XSLTPROC = xsltproc --timing
 FORMAT = xmllint --format
 SUBST = ./subst.pl
-METASTYLESHEET = meta_cic2mathml.xsl
-TMP1 = /tmp/.tmpfile1
-TMP2 = /tmp/.tmpfile2
+METASTYLESHEET = ./meta_cic2mathml.xsl
+TMP1 = .tmpfile1
+TMP2 = .tmpfile2
 
-all: algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl
+all: algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl list.xsl
 
 clean:
-	rm -f algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl
+	rm -f algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl list.xsl
 
 algebra.xsl: algebra.xml $(METASTYLESHEET)
 	@echo "**** PROCESSING algebra.xml ****"
@@ -54,3 +54,12 @@ set.xsl: set.xml $(METASTYLESHEET)
 	@rm $(TMP1)
 	@$(SUBST) oxsl: xsl: set.xsl
 	@$(SUBST) xmlns:oxsl xmlns:xsl set.xsl
+
+list.xsl: list.xml $(METASTYLESHEET)
+	@echo "**** PROCESSING list.xml ****"
+	@$(XSLTPROC) $(METASTYLESHEET) list.xml > $(TMP1)
+	@$(FORMAT) $(TMP1) > $(TMP2)
+	@mv $(TMP2) list.xsl
+	@rm $(TMP1)
+	@$(SUBST) oxsl: xsl: list.xsl
+	@$(SUBST) xmlns:oxsl xmlns:xsl list.xsl
diff --git a/helm/meta_style/algebra.xml b/helm/meta_style/algebra.xml
index 119effa3d..696a19a1b 100644
--- a/helm/meta_style/algebra.xml
+++ b/helm/meta_style/algebra.xml
@@ -1,33 +1,34 @@
 <!DOCTYPE OpList SYSTEM "operator.dtd">
 
-<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML"
+        xmlns:helm="http://www.cs.unibo.it/helm">
 
 <!-- Unary Operations -->
 
 <Operator
  name  = "0"
- uri   = "cic:/Algebra/CSemiGroups/csg_unit.con"
+ uri   = "cic:/Algebra/algebra/CSemiGroups/csg_unit.con"
  arity = "1">
 	<mop tag="ci" helm:xref="$APP-ID">0</mop>
 </Operator>
 
 <Operator
  name  = "1"
- uri   = "cic:/Algebra/CRings/cr_one.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_one.con"
  arity = "1">
 	<mop tag="ci" helm:xref="$APP-ID">1</mop>
 </Operator>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CGroups/cg_inv.con"
+ uri   = "cic:/Algebra/algebra/CGroups/cg_inv.con"
  hide  = "1"
  arity = "1"
  m-tag = "minus"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CMetricFields/CMetric_Fields/cmf_abs.con"
+ uri   = "cic:/Algebra/reals/CMetricFields/cmf_abs.con"
  hide  = "1"
  arity = "2"
  m-tag = "abs"/>
@@ -36,63 +37,63 @@
 
 <Operator
  name  = "SETOID EQUALITY"
- uri   = "cic:/Algebra/CSetoids/cs_eq.con"
+ uri   = "cic:/Algebra/algebra/CSetoids/cs_eq.con"
  hide  = "1"
  arity = "2"
  m-tag = "eq"/>
 
 <Operator
  name  = "APART"
- uri   = "cic:/Algebra/CSetoids/cs_ap.con"
+ uri   = "cic:/Algebra/algebra/CSetoids/cs_ap.con"
  hide  = "1"
  arity = "2"
  m-tag = "neq"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/COrdFields/leEq.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/leEq.con"
  hide  = "1"
  arity = "2"
  m-tag = "leq"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/COrdFields/cof_less.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/cof_less.con"
  hide  = "1"
  arity = "2"
  m-tag = "lt"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/cr_plus.con | cic:/Algebra/CSemiGroups/csg_op.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_plus.con | cic:/Algebra/algebra/CSemiGroups/csg_op.con"
  hide  = "1"
  arity = "2"
  m-tag = "plus"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/cr_minus.con | cic:/Algebra/CGroups/cg_minus.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_minus.con | cic:/Algebra/algebra/CGroups/cg_minus.con"
  hide  = "1"
  arity = "2"
  m-tag = "minus"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/cr_mult.con"
+ uri   = "cic:/Algebra/algebra/CRings/cr_mult.con"
  hide  = "1"
  arity = "2"
  m-tag = "times"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CFields/cf_div.con"
+ uri   = "cic:/Algebra/algebra/CFields/cf_div.con"
  hide  = "1"
  arity = "2"
  m-tag = "divide"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/Ring_constructions/nzpro.con"
+ uri   = "cic:/Algebra/algebra/CRings/nzpro.con"
  cook  = "true"
  arity = "2">
 	<param id="1"/>
@@ -100,14 +101,14 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/exponentiation/nexp.con"
+ uri   = "cic:/Algebra/algebra/CRings/nexp.con"
  cook  = "true"
  arity = "2"
  m-tag = "power"/>
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CRings/exponentiation/nexp_op.con | cic:/Algebra/Expon/Zexp_def/zexp.con"
+ uri   = "cic:/Algebra/algebra/CRings/nexp_op.con | cic:/Algebra/algebra/Expon/zexp.con"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -120,7 +121,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/COrdFields/absSmall.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/absSmall.con"
  hide  = "1"
  arity = "2">
 	<mapp>
@@ -135,7 +136,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Algebra/CPolynomials/CPoly_CRing_ctd/cpoly_apply_fun.con"
+ uri   = "cic:/Algebra/algebra/CPolynomials/cpoly_apply_fun.con"
  cook  = "true"
  arity = "2"> 
  	<mapp>
@@ -147,7 +148,7 @@
 
 <Operator
  name  = "********"
- uri   = "cic:/Algebra/COrdFields/OrdField_Cauchy/seqLimit.con"
+ uri   = "cic:/Algebra/algebra/COrdFields/seqLimit.con"
  cook  = "true"
  arity = "2">
  	<mapp>
@@ -166,7 +167,7 @@
 
 <Operator
  name  = "********"
- uri   = "cic:/Algebra/CSums/Sums/sum0.con"
+ uri   = "cic:/Algebra/algebra/CSums/sum0.con"
  cook  = "true"
  arity = "2">
 	<m:apply helm:xref="$OP-ID">
@@ -185,7 +186,7 @@
 
 <Operator
  name  = "SUM"
- uri   = "cic:/Algebra/CSums/Sums/sum.con"
+ uri   = "cic:/Algebra/algebra/CSums/sum_.con"
  cook  = "true"
  arity = "3">
 	<m:apply helm:xref="$OP-ID">
diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml
index 17fc523cd..a21a51306 100644
--- a/helm/meta_style/arith.xml
+++ b/helm/meta_style/arith.xml
@@ -4,8 +4,6 @@
 
 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
 
-<import href="positive.xsl"/>
-
 <Operator
  name  = "LESS EQUAL"
  uri   = "cic:/Coq/Init/Peano/le.ind | cic:/Coq/ZArith/zarith_aux/Zle.con"
@@ -32,7 +30,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zplus.con"
+ uri   = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/Zplus.con"
  arity = "2"
  m-tag = "plus"/>
 
@@ -44,7 +42,7 @@
  
 <Operator
  name  = "*****"
- uri   = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zmult.con"
+ uri   = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/Zmult.con"
  arity = "2"
  m-tag = "times"/>
 
@@ -56,7 +54,7 @@
 
 <Operator
  name  = "*****"
- uri   = "cic:/Coq/ZArith/fast_integer/fast_integers/Zopp.con"
+ uri   = "cic:/Coq/ZArith/fast_integer/Zopp.con"
  arity = "1"
  m-tag = "minus"/>
 
diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml
index b0681468c..e9da62a62 100644
--- a/helm/meta_style/basic.xml
+++ b/helm/meta_style/basic.xml
@@ -7,16 +7,27 @@
 
 <Operator
  name  = "AND"
- uri   = "cic:/Coq/Init/Logic/Conjunction/and.ind"
+ uri   = "cic:/Coq/Init/Logic/and.ind"
  arity = "2"
  m-tag = "and"/>
 
 <Operator
  name  = "OR"
- uri   = "cic:/Coq/Init/Logic/Disjunction/or.ind"
+ uri   = "cic:/Coq/Init/Logic/or.ind"
  arity = "2"
  m-tag = "or"/>
 
+<Operator
+ name  = "IFF"
+ uri   = "cic:/Coq/Init/Logic/iff.con"
+ arity = "2">
+ 	<mapp>
+		<m:csymbol>iff</m:csymbol>
+		<param id="1"/>
+		<param id="2"/>
+	</mapp>
+</Operator>
+
 <Operator
  name  = "NOT" 
  uri   = "cic:/Coq/Init/Logic/not.con"
@@ -28,14 +39,14 @@
 
 <Operator
  name  = "EQUALITY and TYPE EQUALITY"
- uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  hide  = "1"
  arity = "2"
  m-tag = "eq"/>
 
 <NotOperator
  name  = "NOT-EQ and NOT-EQT"
- uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  hide  = "1"
  arity = "2">
 	<mapp>
@@ -47,7 +58,7 @@
 
 <Operator
  name  = "EXIST"
- uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
+ uri   = "cic:/Coq/Init/Logic/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
  arity = "2">
 	<mapp>
 		<mop tag="exists"/>
@@ -61,7 +72,7 @@
 
 <Operator
  name  = "EXIST"
- uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
+ uri   = "cic:/Coq/Init/Logic/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
  hide  = "1"
  arity = "2">
 	<mapp>
diff --git a/helm/meta_style/list.xml b/helm/meta_style/list.xml
new file mode 100644
index 000000000..9ed07d69b
--- /dev/null
+++ b/helm/meta_style/list.xml
@@ -0,0 +1,60 @@
+<!DOCTYPE OpList SYSTEM "operator.dtd">
+
+<!-- ************************** LISTS ****************************** -->
+
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!-- CSC: manca
+<Operator
+ name  = "CONS"
+ uri   = "cic:/Coq/Lists/PolyList/list.ind"
+ arity = "2"
+ m-tag = "???"/>
+
+<Operator
+ name  = "NIL"
+ uri   = "cic:/Coq/Lists/PolyList/list.ind"
+ arity = "0"
+ m-tag = "???"/> -->
+
+<Operator
+ name  = "APPEND"
+ uri   = "cic:/Coq/Lists/PolyList/app.con"
+ cook  = "true"
+ arity = "2">
+ 	<mapp>
+		<m:csymbol>append</m:csymbol>
+		<param id="1"/>
+		<param id="2"/>
+	</mapp>
+</Operator>
+
+<Operator
+ name  = "IN"
+ uri   = "cic:/Coq/Lists/PolyList/In.con | cic:/Coq/Lists/TheoryList/In_spec.ind | cic:/Coq/Lists/ListSet/set_In.con | cic:/Coq/Lists/ListSet/set_mem.con"
+ cook  = "true"
+ arity = "2"
+ m-tag = "in"/>
+
+<Operator
+ name  = "INCL"
+ uri   = "cic:/Coq/Lists/PolyList/incl.con"
+ cook  = "true"
+ arity = "2"
+ m-tag = "subset"/>
+
+<Operator
+ name  = "INTER"
+ uri   = "cic:/Coq/Lists/ListSet/set_inter.con"
+ cook  = "true"
+ arity = "2"
+ m-tag = "intersect"/>
+
+<Operator
+ name  = "LENGTH"
+ uri   = "cic:/Coq/Lists/PolyList/length.con"
+ cook  = "true"
+ arity = "1"
+ m-tag = "card"/>
+
+</OpList>
diff --git a/helm/meta_style/meta_cic2mathml.xsl b/helm/meta_style/meta_cic2mathml.xsl
index f77890363..072774b5d 100644
--- a/helm/meta_style/meta_cic2mathml.xsl
+++ b/helm/meta_style/meta_cic2mathml.xsl
@@ -47,6 +47,7 @@
 	<oxsl:include href="{@href}"/>
 </xsl:template>
 
+
 <xsl:template match="Operator|NotOperator">
 	<xsl:variable name="uri">
 		<xsl:call-template name="remove_white_spaces">
@@ -79,7 +80,7 @@
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 				</xsl:call-template>
 			</xsl:variable>
-			
+
 			<!-- All uris in uri2 list (if not empty) have MUTIND c-tag -->
 			<xsl:variable name="uri2">
 				<xsl:call-template name="select_uris">
@@ -93,13 +94,24 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri1"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="arity" select="@arity"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 					<xsl:with-param name="const" select="$const"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri1"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="arity" select="@arity"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'CONST'"/>
+					</xsl:call-template>
+				</xsl:if>
 			</xsl:if>
 
 			<xsl:if test="$uri2 != ''">
@@ -107,13 +119,24 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri2"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="arity" select="@arity"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'MUTIND'"/>
 					<xsl:with-param name="const" select="$const"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri2"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="arity" select="@arity"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'MUTIND'"/>
+					</xsl:call-template>	
+				</xsl:if>
 			</xsl:if>
 		</xsl:otherwise>
 	</xsl:choose>
@@ -138,14 +161,14 @@
 	</xsl:variable>
 
 	<xsl:choose>
-		<xsl:when test="$const = 'false' and $not = 'true'">
+		<xsl:when test="$const = 'true' and $not = 'true'">
 			<xsl:call-template name="out_comment">
 				<xsl:with-param name="name" select="concat($uri,': &quot;not&quot; cannot  be applyed to a constant operator')"/>
 			</xsl:call-template>
 		</xsl:when>
 		<xsl:when test="$const = 'true'">
 			<xsl:call-template name="out_comment">
-				<xsl:with-param name="name" select="concat($uri,':  cannot be specified a constant operator when using OpSet element')"/>
+				<xsl:with-param name="name" select="concat($uri,': cannot be specified a constant operator when using OpSet element')"/>
 			</xsl:call-template>
 		</xsl:when>
 		<xsl:otherwise>
@@ -168,11 +191,21 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri1"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'CONST'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template_set">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri1"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'CONST'"/>
+					</xsl:call-template>
+				</xsl:if>
 			</xsl:if>
 
 			<xsl:if test="$uri2 != ''">
@@ -180,11 +213,21 @@
 					<xsl:with-param name="name"  select="@name"/>
 					<xsl:with-param name="not"   select="$not"/>
 					<xsl:with-param name="uri"   select="$uri2"/>
-					<xsl:with-param name="cook"  select="@cook"/>
 					<xsl:with-param name="hide"  select="@hide"/>
 					<xsl:with-param name="m-tag" select="@m-tag"/>
 					<xsl:with-param name="c-tag" select="'MUTIND'"/>
 				</xsl:call-template>
+				<xsl:if test="@cook = 'true'">
+					<xsl:call-template name="out_template_set">
+						<xsl:with-param name="name"  select="@name"/>
+						<xsl:with-param name="not"   select="$not"/>
+						<xsl:with-param name="uri"   select="$uri2"/>
+						<xsl:with-param name="cook"  select="@cook"/>
+						<xsl:with-param name="hide"  select="@hide"/>
+						<xsl:with-param name="m-tag" select="@m-tag"/>
+						<xsl:with-param name="c-tag" select="'MUTIND'"/>
+					</xsl:call-template>	
+				</xsl:if>
 			</xsl:if>
 		</xsl:otherwise>
 	</xsl:choose>
@@ -205,30 +248,26 @@
 	<xsl:param name="m-tag"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
-
-	<xsl:variable name="apply_not">
-		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
-	</xsl:variable>
-
+	
 	<xsl:variable name="match">
 		<xsl:variable name="match_op">
 			<xsl:call-template name="out_match_op">
 				<xsl:with-param name="not"   select="$not"/>
 				<xsl:with-param name="uri"   select="$uri"/>
+				<xsl:with-param name="cook"  select="$cook"/>
 				<xsl:with-param name="c-tag" select="$c-tag"/>
 			</xsl:call-template>
 		</xsl:variable>
-
+		
 		<xsl:variable name="match_child">
-			<xsl:if test="$cook = 'false' or $not = 'true'">
+			<xsl:if test="$const = 'false'">
 				<xsl:choose>
 					<!-- if the operator has been concatenated with not, the root apply node must have only two child -->
-					<xsl:when test="$not = 'true' and $cook = 'true'"> and count(*) = 2</xsl:when>
-					<xsl:when test="$not = 'true' and $cook = 'false'">
+					<xsl:when test="$not = 'true'">
 						<xsl:value-of select="concat(' and count(*) = 2 and count(*[2]/*) = ',$arity + $hide + 1)"/>
 					</xsl:when>
 					<xsl:otherwise>
-						<xsl:value-of select="concat('count(*) = ',$arity + $hide + 1)"/>
+						<xsl:value-of select="concat(' and count(*) = ',$arity + $hide + 1)"/>
 					</xsl:otherwise>
 				</xsl:choose>
 			</xsl:if>
@@ -244,60 +283,21 @@
 		</xsl:choose>
 	</xsl:variable>
 
-	<xsl:variable name="op_uri_attr">
-		<xsl:variable name="tmp_op_uri_attr">
-			<xsl:call-template name="op_uri_attr">
-				<xsl:with-param name="not"   select="$not"/>
-				<xsl:with-param name="c-tag" select="$c-tag"/>
-				<xsl:with-param name="const" select="$const"/>
-			</xsl:call-template>
-		</xsl:variable>
-		<xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
-	</xsl:variable>
-
 	<!--                     TEMPLATE                     -->
 	<xsl:call-template name="out_comment">
 		<xsl:with-param name="name" select="$name"/>
 	</xsl:call-template>
 
 	<oxsl:template match="{$match}" mode="pure">
-		<xsl:choose>
-			<xsl:when test="$cook = 'true'">
-				<oxsl:variable name="no_params">
-					<oxsl:call-template name="get_no_params">
-						<oxsl:with-param name="first_uri"  select="$CICURI"/>
-						<oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
-					</oxsl:call-template>
-				</oxsl:variable>
-				<oxsl:choose>
-					<oxsl:when test="{concat('count(',$apply_not,'*) = $no_params + ',$arity + $hide + 1)}">
-						<xsl:call-template name="out_body">
-							<xsl:with-param name="c-tag" select="$c-tag"/>
-							<xsl:with-param name="m-tag" select="$m-tag"/>
-							<xsl:with-param name="cook"  select="$cook"/>
-							<xsl:with-param name="hide"  select="$hide"/>
-							<xsl:with-param name="arity" select="$arity"/>
-							<xsl:with-param name="not"   select="$not"/>
-							<xsl:with-param name="const" select="$const"/>
-						</xsl:call-template>
-					 </oxsl:when>
-					 <oxsl:otherwise>
-					 	<oxsl:apply-imports/>
-					</oxsl:otherwise>
-				</oxsl:choose>
-			</xsl:when>
-			<xsl:otherwise>
-				<xsl:call-template name="out_body">
-					<xsl:with-param name="c-tag" select="$c-tag"/>
-					<xsl:with-param name="m-tag" select="$m-tag"/>
-					<xsl:with-param name="cook"  select="$cook"/>
-					<xsl:with-param name="hide"  select="$hide"/>
-					<xsl:with-param name="arity" select="$arity"/>
-					<xsl:with-param name="not"   select="$not"/>
-					<xsl:with-param name="const" select="$const"/>
-				</xsl:call-template>
-			</xsl:otherwise>
-		</xsl:choose>
+		<xsl:call-template name="out_body">
+			<xsl:with-param name="c-tag" select="$c-tag"/>
+			<xsl:with-param name="m-tag" select="$m-tag"/>
+			<xsl:with-param name="cook"  select="$cook"/>
+			<xsl:with-param name="hide"  select="$hide"/>
+			<xsl:with-param name="arity" select="$arity"/>
+			<xsl:with-param name="not"   select="$not"/>
+			<xsl:with-param name="const" select="$const"/>
+		</xsl:call-template>
 	</oxsl:template>
 </xsl:template>
 
@@ -310,40 +310,27 @@
 	<xsl:param name="m-tag"/>
 	<xsl:param name="c-tag"/>
 
-	<xsl:variable name="no_params_var">
-		<xsl:if test="$cook = 'true'">$no_params + </xsl:if>
-	</xsl:variable>
-
 	<xsl:variable name="match">
 		<xsl:variable name="match_op">
 			<xsl:call-template name="out_match_op">
-				<xsl:with-param name="not"   select="$not"/> 
+				<xsl:with-param name="not"   select="$not"/>
+				<xsl:with-param name="cook"  select="$cook"/>
 				<xsl:with-param name="uri"   select="$uri"/> 
 				<xsl:with-param name="c-tag" select="$c-tag"/>
 			</xsl:call-template>
 		</xsl:variable>
 		
-		 <xsl:variable name="match_child">
-		 	<xsl:if test="$not = 'true'"> and count(*) = 2</xsl:if>
-		 </xsl:variable>
+		<xsl:variable name="match_child">
+			<xsl:if test="$not = 'true'"> and count(*) = 2</xsl:if>
+		</xsl:variable>
 
-		 <xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
+		<xsl:value-of select="concat('APPLY[',$match_op,$match_child,']')"/>
 	</xsl:variable>
 
 	<xsl:variable name="apply_not">
 		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
 	</xsl:variable>
 
-	<xsl:variable name="op_uri_attr">
-		<xsl:variable name="tmp_op_uri_attr">
-			<xsl:call-template name="op_uri_attr">
-				<xsl:with-param name="not"   select="$not"/>
-				<xsl:with-param name="c-tag" select="$c-tag"/>
-			</xsl:call-template>
-		</xsl:variable>
-		<xsl:value-of select="substring-after(substring-before($tmp_op_uri_attr,'}'),'{')"/>
-	</xsl:variable>
-
 
 	<!--                     TEMPLATE                     -->
 	<xsl:call-template name="out_comment">
@@ -351,17 +338,9 @@
 	</xsl:call-template>
 	
 	<oxsl:template match="{$match}" mode="pure">
-		<xsl:if test="$cook = 'true'">
-			<oxsl:variable name="no_params">
-				<oxsl:call-template name="get_no_params">
-					<oxsl:with-param name="first_uri"  select="$CICURI"/>
-					<oxsl:with-param name="second_uri" select="{$op_uri_attr}"/>
-				</oxsl:call-template>
-			</oxsl:variable>
-		</xsl:if>	
 		<oxsl:choose>
 			<xsl:for-each select="Case">
-				<oxsl:when test="{concat('count(',$apply_not,'*) = ',$no_params_var,@arity + $hide + 1)}">
+				<oxsl:when test="{concat('count(',$apply_not,'*) = ',@arity + $hide + 1)}">
 					<xsl:call-template name="out_body">
 						<xsl:with-param name="c-tag" select="$c-tag"/>
 						<xsl:with-param name="m-tag" select="$m-tag"/>
@@ -392,7 +371,12 @@
 <xsl:template name="out_match_op">
 	<xsl:param name="not"  select="'false'"/>
 	<xsl:param name="uri"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
+
+	<xsl:variable name="instantiate">
+		<xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+	</xsl:variable>
 	
 	<!-- application with not operator -->
 	<xsl:variable name="app_not">
@@ -407,7 +391,7 @@
 
 	<xsl:variable name="app_op">
 		<xsl:if test="$not = 'true'">APPLY[</xsl:if>
-		<xsl:value-of select="concat($c-tag,'[',$uris,']')"/>
+		<xsl:value-of select="concat($instantiate,$c-tag,'[',$uris,']')"/>
 		<xsl:if test="$not = 'true'">]</xsl:if>
 	</xsl:variable>
 
@@ -416,7 +400,6 @@
 
 <xsl:template name="out_params">
 	<xsl:param name="params" select="1"/>
-	<xsl:param name="cook"   select="'false'"/>
 	<xsl:param name="hide"   select="0"/>
 	<xsl:param name="not"    select="'false'"/>
 	<xsl:param name="mode"   select="'noannot'"/>
@@ -427,7 +410,6 @@
 			<xsl:call-template name="param">
 				<xsl:with-param name="id"    select="$params"/>
 				<xsl:with-param name="not"   select="$not"/>
-				<xsl:with-param name="cook"  select="$cook"/>
 				<xsl:with-param name="hide"  select="$hide"/>
 			</xsl:call-template>
 		</xsl:variable>
@@ -436,7 +418,6 @@
 		
 		<xsl:call-template name="out_params">
 			<xsl:with-param name="params" select="$params + 1"/>
-			<xsl:with-param name="cook"   select="$cook"/>
 			<xsl:with-param name="hide"   select="$hide"/>
 			<xsl:with-param name="not"    select="$not"/>
 			<xsl:with-param name="mode"   select="$mode"/>
@@ -445,7 +426,6 @@
 	</xsl:if>
 </xsl:template>
 
-
 <xsl:template name="out_body">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -459,12 +439,13 @@
 		<!--            SIMPLE TRANSFORMATIONS            -->
 		<xsl:when test="count(*) = 0">
 			<xsl:variable name="xref">
-				 <xsl:if test="$const = 'false'">{@id}</xsl:if>
+				<xsl:if test="$const = 'false'">{@id}</xsl:if>
 			</xsl:variable>
 
 			<xsl:variable name="definitionURL">
 				<xsl:call-template name="op_uri_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$const"/>
 				</xsl:call-template>
@@ -473,6 +454,7 @@
 			 <xsl:variable name="helm:xref">
 			 	<xsl:call-template name="op_id_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$const"/>
 				</xsl:call-template>
@@ -491,8 +473,7 @@
 				</xsl:element>
 				<!--            PARAMS            -->
 				<xsl:call-template name="out_params">
-					<xsl:with-param name="cook"   select="$cook"/>
-					<xsl:with-param name="hide"   select="$hide"/>	
+					<xsl:with-param name="hide"   select="$hide"/>					
 					<xsl:with-param name="not"    select="$not"/>
 					<xsl:with-param name="arity"  select="$arity"/>
 				</xsl:call-template>
@@ -512,6 +493,7 @@
 	</xsl:choose>
 </xsl:template>
 
+
 <xsl:template name="out_mvar">
 	<xsl:param name="vname"/>
 	
@@ -531,7 +513,6 @@
 <xsl:template name="out_choose_binder">
 	<xsl:param name="binded_params" select="''"/>
 	<xsl:param name="not"           select="'false'"/>
-	<xsl:param name="cook"          select="'false'"/>
 	<xsl:param name="hide"          select="0"/>
 	<xsl:param name="binder"/>
 	
@@ -541,7 +522,6 @@
 				<xsl:call-template name="out_choose_binder">
 					<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
 					<xsl:with-param name="not"           select="$not"/>
-					<xsl:with-param name="cook"          select="$cook"/>
 					<xsl:with-param name="hide"          select="$hide"/>
 					<xsl:with-param name="binder"        select="$binder"/>
 				</xsl:call-template>
@@ -549,7 +529,6 @@
 				<xsl:call-template name="out_choose_binder">
 					<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
 					<xsl:with-param name="not"           select="$not"/>
-					<xsl:with-param name="cook"          select="$cook"/>
 					<xsl:with-param name="hide"          select="$hide"/>
 					<xsl:with-param name="binder"        select="$binder"/>
 				</xsl:call-template>
@@ -559,7 +538,6 @@
 					<xsl:call-template name="param">
 						<xsl:with-param name="id"    select="$binded_params"/>
 						<xsl:with-param name="not"   select="$not"/>
-						<xsl:with-param name="cook"  select="$cook"/>
 						<xsl:with-param name="hide"  select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -572,6 +550,7 @@
 	</xsl:if>
 </xsl:template>
 
+
 <!-- *********************************************************************** -->
 <!--                     META LANGUAGE FOR MathML                            --> 
 <!-- *********************************************************************** -->
@@ -590,6 +569,7 @@
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@xref"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
 					<xsl:with-param name="not"   select="$not"/>
@@ -604,6 +584,7 @@
 
 	<m:apply helm:xref="{$helm:xref}">
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"   select="$cook"/>
 			<xsl:with-param name="c-tag"  select="$c-tag"/>
 			<xsl:with-param name="hide"   select="$hide"/>
 			<xsl:with-param name="arity"  select="$arity"/>
@@ -623,7 +604,6 @@
 	</m:apply>
 </xsl:template>
 
-
 <xsl:template match="mop">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -638,6 +618,7 @@
 			<xsl:when test="@definitionURL">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@definitionURL"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
@@ -648,6 +629,7 @@
 			<xsl:otherwise>
 				<xsl:call-template name="op_uri_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$const"/>
 				</xsl:call-template>
@@ -661,6 +643,7 @@
 			<xsl:when test="@xref">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="@xref"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
@@ -671,6 +654,7 @@
 			<xsl:otherwise>
 				<xsl:call-template name="op_id_attr">
 					<xsl:with-param name="not"   select="$not"/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="const" select="$const"/>
 				</xsl:call-template>
@@ -687,6 +671,7 @@
 		</xsl:attribute>
 		
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"   select="$cook"/>
 			<xsl:with-param name="c-tag"  select="$c-tag"/>
 			<xsl:with-param name="hide"   select="$hide"/>
 			<xsl:with-param name="arity"  select="$arity"/>
@@ -706,8 +691,8 @@
 	</xsl:element>
 </xsl:template>
 
+
 <xsl:template match="param">
-	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="hide" select="0"/>
 	<xsl:param name="not"  select="'false'"/>
 
@@ -715,7 +700,6 @@
 		<xsl:call-template name="param">
 			<xsl:with-param name="id"    select="@id"/>
 			<xsl:with-param name="not"   select="$not"/>
-			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="hide"  select="$hide"/>
 		</xsl:call-template>
 	</xsl:variable>
@@ -743,6 +727,7 @@
 	</xsl:choose>
 </xsl:template>
 
+
 <xsl:template match="m:*">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -753,6 +738,7 @@
 	
 	<xsl:copy>
 		<xsl:call-template name="copy_attributes">
+			<xsl:with-param name="cook"  select="$cook"/>
 			<xsl:with-param name="c-tag" select="$c-tag"/>
 			<xsl:with-param name="hide"  select="$hide"/>
 			<xsl:with-param name="arity" select="$arity"/>
@@ -771,6 +757,7 @@
 	</xsl:copy>
 </xsl:template>
 
+
 <xsl:template match="mbvar">
 	<xsl:param name="c-tag"/>
 	<xsl:param name="cook"  select="'false'"/>
@@ -790,12 +777,11 @@
 		<xsl:call-template name="test_on_lambda">
 			<xsl:with-param name="binded_params" select="$binded_params"/>
 			<xsl:with-param name="not"           select="$not"/>
-			<xsl:with-param name="cook"          select="$cook"/>
 			<xsl:with-param name="hide"          select="$hide"/>
 		</xsl:call-template>
 	</xsl:variable>
 
-	<xsl:variable name="binder">/target/@binder</xsl:variable>
+	<xsl:variable name="binder">/decl/@binder</xsl:variable>
 
 	<xsl:choose>
 		<xsl:when test="$binded_params != ''">
@@ -812,11 +798,10 @@
 											<xsl:with-param name="binded_params" select="$binded_params"/>
 											<xsl:with-param name="not"           select="$not"/>
 											<xsl:with-param name="hide"          select="$hide"/>
-											<xsl:with-param name="cook"          select="$cook"/>
 											<xsl:with-param name="binder"        select="$binder"/>
 										</xsl:call-template>
 									</oxsl:choose>
-								</oxsl:variable>
+ 								</oxsl:variable>
 								<oxsl:call-template name="insert_subscript">
 									<oxsl:with-param name="node_value" select="$binder"/>
 								</oxsl:call-template>
@@ -827,11 +812,10 @@
 									<xsl:call-template name="param">
 										<xsl:with-param name="id"    select="$binded_params"/>
 										<xsl:with-param name="not"   select="$not"/>
-										<xsl:with-param name="cook"  select="$cook"/>
 										<xsl:with-param name="hide"  select="$hide"/>
 									</xsl:call-template>
-								</xsl:variable>
-							
+								</xsl:variable>								
+
 								<oxsl:call-template name="insert_subscript">
 									<oxsl:with-param name="node_value" select="{concat($param,$binder)}"/>
 								</oxsl:call-template>
@@ -877,6 +861,8 @@
 	</xsl:choose>
 </xsl:template>
 
+
+
 <xsl:template match="mvar">
 	<xsl:call-template name="out_mvar">
 		<xsl:with-param name="vname" select="@name"/>
@@ -884,7 +870,6 @@
 </xsl:template>
 
 
-
 <!-- *********************************************************************** -->
 <!--                          AUXILIARY FUNCTIONS                            -->
 <!-- *********************************************************************** -->
@@ -1004,7 +989,6 @@
 <xsl:template name="test_on_lambda">
 	<xsl:param name="binded_params" select="''"/>
 	<xsl:param name="not"           select="'false'"/>
-	<xsl:param name="cook"          select="'false'"/>
 	<xsl:param name="hide"          select="0"/>
 	
 	<xsl:if test="$binded_params != ''">
@@ -1014,7 +998,6 @@
 					<xsl:call-template name="test_on_lambda">
 						<xsl:with-param name="binded_params" select="substring-before($binded_params,'+')"/>
 						<xsl:with-param name="not"           select="$not"/>
-						<xsl:with-param name="cook"          select="$cook"/>
 						<xsl:with-param name="hide"          select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1023,7 +1006,6 @@
 					<xsl:call-template name="test_on_lambda">
 						<xsl:with-param name="binded_params" select="substring-after($binded_params,'+')"/>
 						<xsl:with-param name="not"           select="$not"/>
-						<xsl:with-param name="cook"          select="$cook"/>
 						<xsl:with-param name="hide"          select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1035,7 +1017,6 @@
 					<xsl:call-template name="param">
 						<xsl:with-param name="id"    select="$binded_params"/>
 						<xsl:with-param name="not"   select="$not"/>
-						<xsl:with-param name="cook"  select="$cook"/>
 						<xsl:with-param name="hide"  select="$hide"/>
 					</xsl:call-template>
 				</xsl:variable>
@@ -1140,29 +1121,26 @@
 <xsl:template name="param">
 	<xsl:param name="id"/>
 	<xsl:param name="not"   select="'false'"/>
-	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="hide"  select="0"/>
 
 	<xsl:variable name="apply_not">
 		<xsl:if test="$not = 'true'">*[2]/</xsl:if>
 	</xsl:variable>
 
-	<xsl:variable name="no_params_var">
-		<xsl:if test="$cook = 'true'">$no_params+</xsl:if>
-	</xsl:variable>
-
-	<xsl:value-of select="concat($apply_not,'*[',$no_params_var,$id + $hide + 1,']')"/>
+	<xsl:value-of select="concat($apply_not,'*[',$id + $hide + 1,']')"/>
 </xsl:template>
 
 <!-- Returns a xpath string with the location of the operator uri attribute -->
 <xsl:template name="op_uri_attr">
 	<xsl:param name="not"   select="'false'"/>
+	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
 
 	<xsl:call-template name="op_attr">
 		<xsl:with-param name="attr_type" select="'@uri'"/>
 		<xsl:with-param name="not"       select="$not"/>
+		<xsl:with-param name="cook"      select="$cook"/>
 		<xsl:with-param name="c-tag"     select="$c-tag"/>
 		<xsl:with-param name="const"     select="$const"/>
 	</xsl:call-template>
@@ -1171,12 +1149,14 @@
 <!-- Returns a xpath string with the location of the operator id attribute -->
 <xsl:template name="op_id_attr">
 	<xsl:param name="not"  select="'false'"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
 	
 	<xsl:call-template name="op_attr">
 		<xsl:with-param name="attr_type" select="'@id'"/>
 		<xsl:with-param name="not"       select="$not"/>
+		<xsl:with-param name="cook"      select="$cook"/>
 		<xsl:with-param name="c-tag"     select="$c-tag"/>
 		<xsl:with-param name="const"     select="$const"/>
 	</xsl:call-template>
@@ -1187,8 +1167,13 @@
 <xsl:template name="op_attr">
 	<xsl:param name="attr_type"/>
 	<xsl:param name="not"  select="'false'"/>
+	<xsl:param name="cook" select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="const" select="'false'"/>
+	
+	<xsl:variable name="instantiate">
+		<xsl:if test="$cook = 'true'">instantiate/</xsl:if>
+	</xsl:variable>
 
 	<xsl:variable name="apply">
 		<xsl:if test="$not = 'true'">APPLY/</xsl:if>
@@ -1199,12 +1184,13 @@
 			<xsl:value-of select="concat('{',$attr_type,'}')"/>	
 		</xsl:when>
 		<xsl:otherwise>
-			<xsl:value-of select="concat('{',$apply,$c-tag,'/',$attr_type,'}')"/> 			
+			<xsl:value-of select="concat('{',$apply,$instantiate,$c-tag,'/',$attr_type,'}')"/> 			
 		</xsl:otherwise>
 	</xsl:choose>
 </xsl:template>
 
 <xsl:template name="copy_attributes">
+	<xsl:param name="cook"   select="'false'"/>
 	<xsl:param name="c-tag"/>
 	<xsl:param name="hide"   select="0"/>
 	<xsl:param name="arity"  select="0"/>
@@ -1232,6 +1218,7 @@
 			<xsl:attribute name="{$name}">
 				<xsl:call-template name="set_attribute">
 					<xsl:with-param name="attr"  select="."/>
+					<xsl:with-param name="cook"  select="$cook"/>
 					<xsl:with-param name="c-tag" select="$c-tag"/>
 					<xsl:with-param name="hide"  select="$hide"/>
 					<xsl:with-param name="arity" select="$arity"/>
@@ -1265,6 +1252,7 @@
 <xsl:template name="set_attribute">
 	<xsl:param name="attr"/>
 	<xsl:param name="c-tag"/>
+	<xsl:param name="cook"  select="'false'"/>
 	<xsl:param name="hide"  select="0"/>
 	<xsl:param name="arity" select="0"/>
 	<xsl:param name="not"   select="'false'"/>
@@ -1281,10 +1269,11 @@
 					<xsl:otherwise>@uri</xsl:otherwise>
 				</xsl:choose>
 			</xsl:variable>
-
+			
 			<xsl:call-template name="op_attr">
 				<xsl:with-param name="attr_type" select="$attr_type"/>
 				<xsl:with-param name="not"       select="$not"/>
+				<xsl:with-param name="cook"      select="$cook"/>
 				<xsl:with-param name="c-tag"     select="$c-tag"/>
 				<xsl:with-param name="const"     select="$const"/>
 			</xsl:call-template>
diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl
index f52b64702..e337b663e 100644
--- a/helm/meta_style/positive.xsl
+++ b/helm/meta_style/positive.xsl
@@ -73,7 +73,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
 
 
 
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
    <xsl:apply-templates select="*[2]" mode="Zpositive">
     <xsl:with-param name="base" select="0"/>
     <xsl:with-param name="exp" select="1"/>
@@ -81,7 +81,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
    </xsl:apply-templates>
 </xsl:template>
  
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='3'] and count(*)=2]" mode="pure">
    <m:apply helm:xref="{@id}">
     <m:minus definitionURL="{*[1]/@uri}" helm:xref="{*[1]/@id}"/>
     <xsl:apply-templates select="*[2]" mode="Zpositive">
@@ -92,13 +92,13 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
    </m:apply>
 </xsl:template>
 
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/Z.ind' and @noConstr='1']" mode="pure">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/Z.ind' and @noConstr='1']" mode="pure">
    <m:ci definitionURL="{@uri}" helm:xref="{@id}">0</m:ci>
 </xsl:template>
 
 <!-- prova di notazione per positive -->
 
-<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind']]" mode="pure">
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/positive.ind']]" mode="pure">
    <xsl:apply-templates select="." mode="Zpositive">
     <xsl:with-param name="base" select="0"/>
     <xsl:with-param name="exp" select="1"/>
@@ -106,7 +106,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
    </xsl:apply-templates>
 </xsl:template>
 
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3']" mode="pure">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='3']" mode="pure">
  <m:ci definitionURL="{@uri}" helm:xref="{@id}">1</m:ci>
 </xsl:template> 
 
@@ -116,7 +116,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
  <xsl:param name="iden" select="''"/>
  <xsl:choose>
   <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT'
-and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='1']">
+and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='1']">
    <xsl:apply-templates select="*[2]" mode="Zpositive">
     <xsl:with-param name="base" select="$base + $exp"/>
     <xsl:with-param name="exp" select="2 * $exp"/>
@@ -124,14 +124,14 @@ and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr
    </xsl:apply-templates>
   </xsl:when>
   <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT' 
-and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='2']">
+and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='2']">
    <xsl:apply-templates select="*[2]" mode="Zpositive">
     <xsl:with-param name="base" select="$base"/>
     <xsl:with-param name="exp" select="2 * $exp"/>
     <xsl:with-param name="iden" select="$iden"/>
    </xsl:apply-templates>
   </xsl:when>
-  <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr='3'">
+  <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='3'">
    <m:ci helm:xref="{$iden}"><xsl:value-of select="$base + $exp"/></m:ci>
   </xsl:when>
   <xsl:otherwise>
@@ -173,5 +173,46 @@ and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr
  </xsl:choose>
 </xsl:template>
 
+<!-- **************************** Reals ******************************** -->
+
+<xsl:template match="APPLY[CONST[position() = 1 and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and count(*) = 3]" mode="pure">
+  <xsl:variable name="result">
+   <xsl:apply-templates select="." mode="reals"/>
+  </xsl:variable>
+  <xsl:choose>
+   <xsl:when test="string($result) = ''">
+    <m:apply helm:xref="{@id}">
+      <m:plus xmlns:m="http://www.w3.org/1998/Math/MathML" definitionURL="{CONST[1]/@uri}" helm:xref="{CONST[1]/@id}"/>
+      <xsl:apply-templates select="*[2]" mode="noannot"/>
+      <xsl:apply-templates select="*[3]" mode="noannot"/>
+    </m:apply>
+   </xsl:when>
+   <xsl:otherwise>
+    <m:cn helm:xref="{CONST[1]/@id}"><xsl:value-of select="$result"/></m:cn>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+<xsl:template match="APPLY[*[position() = 1 and name()='CONST' and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and *[position() = 2 and name()='CONST' and @uri='cic:/Coq/Reals/Rdefinitions/R1.con'] and count(*) = 3]" mode="reals">
+  <xsl:param name="real_counter" select="0"/>
+  <xsl:variable name="result">
+   <xsl:apply-templates select="*[3]" mode="reals">
+    <xsl:with-param name="real_counter" select="$real_counter + 1"/>
+   </xsl:apply-templates>
+  </xsl:variable>
+  <xsl:choose>
+   <xsl:when test="string($result) = ''"/>
+   <xsl:otherwise>
+    <xsl:value-of select="$result"/>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+<xsl:template match="CONST[@uri='cic:/Coq/Reals/Rdefinitions/R1.con']" mode="reals">
+  <xsl:param name="real_counter" select="0"/>
+  <xsl:value-of select="$real_counter + 1"/>
+</xsl:template>
+
+<xsl:template match="*" mode="reals"/>
 
 </xsl:stylesheet>
diff --git a/helm/meta_style/set.xml b/helm/meta_style/set.xml
index f1e888d98..0dbcd3761 100644
--- a/helm/meta_style/set.xml
+++ b/helm/meta_style/set.xml
@@ -1,12 +1,13 @@
 <!DOCTYPE OpList SYSTEM "operator.dtd">
 
-<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML"
+        xmlns:helm="http://www.cs.unibo.it/helm">
 
 <import href="modeset.xsl"/>
 
 <Operator
  name  = "IN"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
+ uri   = "cic:/Coq/Sets/Ensembles/In.con"
  cook  = "true"
  arity = "2">
  	<mapp>
@@ -18,7 +19,7 @@
 
 <NotOperator
  name  = "NOT IN"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
+ uri   = "cic:/Coq/Sets/Ensembles/In.con"
  cook  = "true"
  arity = "2">
  	<mapp>
@@ -28,86 +29,95 @@
 	</mapp>
 </NotOperator>
 
-<OpSet
+<Operator
  name  = "EMPTY SET"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
- cook  = "true">
-	
-	<Case arity="0">
-		<mop tag="set" helm:xref="$APP-ID"/>
-	</Case>
-
-	<Case arity="1">
+ uri   = "cic:/Coq/Sets/Ensembles/Empty_set.ind"
+ cook  = "true"
+ arity = "1">
 		<mapp>
-			<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 			<param id="1"/>
 			<mop tag="set" helm:xref="$APP-ID"/>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
- name  = "SINGLETON"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind"
+<Operator
+ name  = "EMPTY SET"
+ uri   = "cic:/Coq/Sets/Ensembles/Empty_set.ind"
  cook  = "true">
+ 	<mop tag="set" helm:xref="$APP-ID"/>
+</Operator>
 
- 	<Case arity="1">
+
+<Operator
+ name  = "SINGLETON"
+ uri   = "cic:/Coq/Sets/Ensembles/Singleton.ind"
+ cook  = "true"
+ arity = "1">
  		<mop tag="set" helm:xref="$APP-ID">
 			<param id="1"/>
 		</mop>
-	</Case>
+</Operator>
 
- 	<Case arity="2">
+<Operator
+ name  = "SINGLETON"
+ uri   = "cic:/Coq/Sets/Ensembles/Singleton.ind"
+ cook  = "true"
+ arity = "2">
 		<mapp>
-			<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 			<param id="2"/>
 			<m:set definitionURL="$OP-URI">
 				<param id="1"/>
 			</m:set>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "COUPLE"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind"
- cook  = "true">
- 	
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Couple.ind"
+ cook  = "true"
+ arity = "2">
 		<mop tag="set" helm:xref="$APP-ID">
 			<param id="1"/>
 			<param id="2"/>
 		</mop>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "COUPLE"
+ uri   = "cic:/Coq/Sets/Ensembles/Couple.ind"
+ cook  = "true"
+ arity = "3">
 		<mapp>
-			<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 			<param id="3"/>
 			<m:set definitionURL="$OP-URI">
 				<param id="1"/>
 				<param id="2"/>
 			</m:set>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "TRIPLE"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind"
- cook  = "true">
- 
-	<Case arity="3">
+ uri   = "cic:/Coq/Sets/Ensembles/Triple.ind"
+ cook  = "true"
+ arity = "3">
 		<mop tag="set">
 			<param id="1"/>
 			<param id="2"/>
 			<param id="3"/>
 		</mop>
-	</Case>
+</Operator>
  
-	<Case arity="4">
+<Operator
+ name  = "TRIPLE"
+ uri   = "cic:/Coq/Sets/Ensembles/Triple.ind"
+ cook  = "true"
+ arity = "4">
 		<mapp>
-			<m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
+			<m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 			<param id="4"/>
 			<m:set definitionURL="$OP-URI">
 				<param id="1"/>
@@ -115,23 +125,25 @@
 				<param id="3"/>
 			</m:set>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "INTERSECTION"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Intersection.ind"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="intersect"/>
 			<param id="1" mode="set"/>
 			<param id="2" mode="set"/>
 		</mapp>
-	</Case>
+</Operator>
 
- 	<Case arity="3">
+<Operator
+ name  = "INTERSECTION"
+ uri   = "cic:/Coq/Sets/Ensembles/Intersection.ind"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>
@@ -141,23 +153,25 @@
 				<param id="2" mode="set"/>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "UNION"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Union.ind"
- cook  = "true">
-	
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Union.ind"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="union"/>
 			<param id="1" mode="set"/>
 			<param id="2" mode="set"/>		
 		</mapp>
-	</Case>
+</Operator>
  
-	<Case arity="3">
+<Operator
+ name  = "UNION"
+ uri   = "cic:/Coq/Sets/Ensembles/Union.ind"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>	
@@ -167,12 +181,11 @@
 				<param id="2" mode="set"/>
 			</m:apply>	
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
 <Operator
  name  = "INCLUDED"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Included.con"
+ uri   = "cic:/Coq/Sets/Ensembles/Included.con"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -184,7 +197,7 @@
 
 <Operator
  name  = "STRICTLY INCLUDED"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con"
+ uri   = "cic:/Coq/Sets/Ensembles/Strict_Included.con"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -194,20 +207,23 @@
 	</mapp>
 </Operator>
 
-<OpSet
+<Operator
  name  = "SET-DIFF"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Setminus.con"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="setdiff"/>
 			<param id="1" mode="set"/>
 			<param id="2" mode="set"/>
 		</mapp>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "SET-DIFF"
+ uri   = "cic:/Coq/Sets/Ensembles/Setminus.con"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>	
@@ -217,15 +233,13 @@
 				<param id="2" mode="set"/>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "ADD-ELEM"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Add.con"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Add.con"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="union"/>
 			<param id="1" mode="set"/>
@@ -233,9 +247,13 @@
 				<param id="2" mode="set"/>
 			</m:set>
 		</mapp>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "ADD-ELEM"
+ uri   = "cic:/Coq/Sets/Ensembles/Add.con"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>
@@ -247,15 +265,13 @@
 				</m:set>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
-<OpSet
+<Operator
  name  = "SUBTRACT-ELEM"
- uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con"
- cook  = "true">
-
-	<Case arity="2">
+ uri   = "cic:/Coq/Sets/Ensembles/Subtract.con"
+ cook  = "true"
+ arity = "2">
 		<mapp>
 			<mop tag="setdiff"/>
 			<param id="1" mode="set"/>
@@ -263,9 +279,13 @@
 				<param id="2"/>
 			</m:set>
 		</mapp>
-	</Case>
+</Operator>
 
-	<Case arity="3">
+<Operator
+ name  = "SUBTRACT-ELEM"
+ uri   = "cic:/Coq/Sets/Ensembles/Subtract.con"
+ cook  = "true"
+ arity = "3">
 		<mapp>
 			<m:in/>
 			<param id="3"/>
@@ -277,12 +297,11 @@
 				</m:set>
 			</m:apply>
 		</mapp>
-	</Case>
-</OpSet>
+</Operator>
 
 <Operator
  name  = "CARD"
- uri   = "cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind"
+ uri   = "cic:/Coq/Sets/Finite_sets/cardinal.ind"
  cook  = "true"
  arity = "2">
 	<mapp>
@@ -297,7 +316,7 @@
 
 <Operator
  name  = "SIGMA"
- uri   = "cic:/Coq/Init/Specif/Subsets/sig.ind"
+ uri   = "cic:/Coq/Init/Specif/sig.ind"
  arity = "2">
 	<m:set>
 		<mbvar name="x">
diff --git a/helm/meta_style/xslt_index.txt b/helm/meta_style/xslt_index.txt
index 889ce4c6c..2f683f28d 100644
--- a/helm/meta_style/xslt_index.txt
+++ b/helm/meta_style/xslt_index.txt
@@ -3,5 +3,6 @@ arith.xsl
 basic.xsl
 reals.xsl
 set.xsl
+list.xsl
 positive.xsl
 modeset.xsl
diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl
index 97f259d67..9cc298f09 100644
--- a/helm/style/annotatedcont.xsl
+++ b/helm/style/annotatedcont.xsl
@@ -35,9 +35,9 @@
 
 <xsl:import href="objcontent.xsl"/>
 
-<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
+<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate|ConstantType|ConstantBody|CurrentProof|InductiveDefinition|Variable"/>
 
-<xsl:template match="Definition|Axiom|CurrentProof|InductiveDefinition|Variable">
+<xsl:template match="ConstantType|ConstantBody|CurrentProof|InductiveDefinition|Variable">
     <xsl:variable name="id" select="@id"/>
     <xsl:choose>
     <xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
@@ -51,7 +51,7 @@
     </xsl:choose>
 </xsl:template>
 
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate">
     <xsl:variable name="id" select="@id"/>
     <xsl:choose>
     <xsl:when test="$annotations='yes' and $CICAnnotations/Annotations/Annotation[@of=$id]">
diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index e60a85051..001ff876d 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -37,6 +37,7 @@
                               xmlns:helm="http://www.cs.unibo.it/helm">
 
 <xsl:include href="params.xsl"/>
+<xsl:include href="ite.xsl"/>
 <!-- adesso sono preprocessate -->
 <!-- <xsl:include href="coercions.xsl"/> -->
 
@@ -62,63 +63,98 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 <!-- CIC TERMS -->
 
+
 <xsl:template match="LAMBDA" 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="target/@binder"/></xsl:with-param></xsl:call-template>
-      </m:ci>
-      <m:type>
-       <xsl:apply-templates select="source/*[1]" mode="noannot"/>
-      </m:type>
-     </m:bvar>
-     <xsl:apply-templates select="target/*[1]" mode="noannot"/>
-    </m:lambda>
+	<xsl:apply-templates select="*[1]" mode="lambda"/>
+</xsl:template>
+
+<xsl:template match="decl" mode="lambda">
+	<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"/>
+	</m:lambda>
+</xsl:template>
+
+
+<xsl:template match="target" mode="lambda">
+	<xsl:apply-templates select="*[1]" mode="noannot"/>
 </xsl:template>
 
+
 <xsl:template match="LETIN" mode="pure">
+	<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_pure">	
     <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="letintarget/@binder"/></xsl:with-param></xsl:call-template>
+       <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="letintarget/*[1]" mode="noannot"/>
+     <xsl:apply-templates select="following-sibling::*[1]" mode="letin_pure"/>
     </m:apply>
 </xsl:template>
 
+
+<xsl:template match="target" mode="letin_pure">
+	<xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
+
 <xsl:template match="PROD" mode="pure">
-    <m:apply helm:xref="{@id}">
-     <xsl:choose>
-     <xsl:when test="string(target/@binder)= &quot;&quot;">
-      <m:csymbol>arrow</m:csymbol>
-      <xsl:apply-templates select="source/*[1]" mode="noannot"/>
-     </xsl:when>
-     <xsl:otherwise>
+	<xsl:apply-templates select="*[1]" mode="prod"/>
+</xsl:template>
+
+
+<xsl:template match="decl" mode="prod">
+     <m:apply helm:xref="{@id}">
       <xsl:choose>
-       <xsl:when test="@type = 'Prop'">
-        <m:csymbol>forall</m:csymbol>
+       <xsl:when test="string(@binder)= &quot;&quot;">
+        <m:csymbol>arrow</m:csymbol>
+        <xsl:apply-templates select="*[1]" mode="noannot"/>
        </xsl:when>
        <xsl:otherwise>
-        <m:csymbol>prod</m:csymbol>
+        <xsl:choose>
+         <xsl:when test="../@type = 'Prop'">
+          <m:csymbol>forall</m:csymbol>
+         </xsl:when>
+         <xsl:otherwise>
+          <m:csymbol>prod</m:csymbol>
+         </xsl:otherwise>
+        </xsl:choose>
+        <m:bvar>
+         <m:ci>
+          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@binder"/></xsl:with-param></xsl:call-template>
+         </m:ci>
+         <m:type>
+          <xsl:apply-templates select="*[1]" mode="noannot"/>
+         </m:type>
+        </m:bvar>
        </xsl:otherwise>
       </xsl:choose>
-       <m:bvar>
-        <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
-        </m:ci>
-        <m:type>
-         <xsl:apply-templates select="source/*[1]" mode="noannot"/>
-        </m:type>
-       </m:bvar>
-     </xsl:otherwise>
-     </xsl:choose>
-     <xsl:apply-templates select="target/*[1]" mode="noannot"/>
-    </m:apply>
+     <xsl:apply-templates select="following-sibling::*[1]" mode="prod"/> 
+     </m:apply>
+</xsl:template>
+
+	 
+<xsl:template match="target" mode="prod">
+	<xsl:apply-templates select="*[1]" mode="noannot"/>
 </xsl:template>
 
+
 <xsl:template match="CAST" mode="pure">
     <m:apply helm:xref="{@id}">
      <m:csymbol>cast</m:csymbol>
@@ -126,12 +162,14 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:apply>
 </xsl:template>
 
+
 <xsl:template match="REL" mode="pure">
     <m:ci helm:xref="{@id}">
      <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>
 </xsl:template>
 
+
 <xsl:template match="SORT" mode="pure">
     <m:apply helm:xref="{@id}">
      <m:csymbol>
@@ -140,6 +178,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:apply>
 </xsl:template>
 
+
 <xsl:template match="APPLY" mode="pure">
       <m:apply helm:xref="{@id}">
        <m:csymbol>app</m:csymbol>
@@ -147,6 +186,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
       </m:apply>
 </xsl:template>
 
+
 <!-- Gestione senza pre-processing -->
 <!-- 
 <xsl:template match="APPLY" mode="pure">
@@ -163,10 +203,12 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 
 <xsl:template match="VAR" mode="pure">
     <m:ci helm:xref="{@id}">
-     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="substring-after(@relUri,&quot;,&quot;)"/></xsl:with-param></xsl:call-template>
+     <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:call-template name="name_of_uri_bis">
+      <xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:with-param></xsl:call-template>
     </m:ci>
 </xsl:template>
 
+
 <xsl:template match="META" mode="pure">
    <m:apply helm:xref="{@id}">
     <m:csymbol>meta</m:csymbol>
@@ -191,6 +233,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
    </m:apply>
 </xsl:template>
 
+
 <xsl:template match="CONST" mode="pure">
    <m:ci definitionURL="{@uri}" helm:xref="{@id}">
       <xsl:call-template name="insert_subscript">
@@ -203,6 +246,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
    </m:ci>
 </xsl:template>
 
+
 <xsl:template match="MUTIND" mode="pure">
     <m:ci definitionURL="{@uri}" helm:xref="{@id}">
      <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
@@ -211,6 +255,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:ci>
 </xsl:template>
 
+
 <xsl:template match="MUTCONSTRUCT" mode="pure">
     <m:ci definitionURL="{@uri}" helm:xref="{@id}">
      <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="@uri"/></xsl:call-template></xsl:variable>
@@ -220,6 +265,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:ci>
 </xsl:template>
 
+
 <xsl:template match="MUTCASE" mode="pure">
     <xsl:variable name="Tindex"><xsl:value-of select="@noType"/></xsl:variable>
     <xsl:variable name="Turi"><xsl:value-of select="@uriType"/></xsl:variable>
@@ -258,6 +304,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:apply>
 </xsl:template>
 
+
 <xsl:template match="FIX" mode="pure">
     <m:apply helm:xref="{@id}">
      <xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
@@ -267,6 +314,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:apply>
 </xsl:template>
 
+
 <xsl:template match="COFIX" mode="pure">
    <m:apply helm:xref="{@id}">
      <xsl:variable name="findex"><xsl:value-of select="@noFun"/></xsl:variable>
@@ -276,6 +324,37 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:apply>
 </xsl:template>
 
+<xsl:template match="instantiate" mode="pure">
+	<m:apply>
+         <xsl:if test="@id">
+          <xsl:attribute name="helm:xref">
+	   <xsl:value-of select="@id"/>
+          </xsl:attribute>
+         </xsl:if>
+	 <m:csymbol>inst</m:csymbol>
+	 <xsl:apply-templates mode="noannot" select="*[1]" />
+	 <xsl:for-each select="arg">
+          <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>
+</xsl:template>
+
 <!-- ELEMENTS OF CIC TERMS -->
 
 <xsl:template match="FixFunction" mode="pure">
@@ -286,6 +365,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     <xsl:apply-templates select="body/*[1]" mode="noannot"/>
 </xsl:template>
 
+
 <xsl:template match="CofixFunction" mode="pure">
     <m:bvar>
      <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="@name"/></xsl:with-param></xsl:call-template></m:ci>
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 856fd6971..56231b2bc 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -39,6 +39,7 @@
 <xsl:include href="html_init.xsl"/>
 <xsl:include href="html_set.xsl"/>
 <xsl:include href="html_reals.xsl"/>
+<xsl:include href="html_ccorns.xsl"/>
 
 <xsl:variable name="showcast" select="0"/>
 
@@ -69,6 +70,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 +121,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>
@@ -215,6 +228,12 @@
 
 <xsl:template name="make_indent">
  <xsl:param name="current_indent" select="0"/>
+ <!-- non funziona bene con netscape !!! 
+ <span>
+  <xsl:attribute name="style">
+   <xsl:value-of select="concat('margin-left:',string($current_indent div 3), 'em')"/>
+  </xsl:attribute>
+ </span> -->
   <xsl:if test="$current_indent > 0">
    <xsl:text>&#x00a0;</xsl:text>
    <xsl:call-template name="make_indent">
@@ -311,6 +330,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>
@@ -325,7 +368,7 @@
     <xsl:when test="$name='cast'">
      <xsl:text>(</xsl:text>
      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     <xsl:text>:></xsl:text>
+     <xsl:text>:</xsl:text>
      <xsl:apply-templates mode="inline" select="*[position()=3]"/>
      <xsl:text>)</xsl:text>
     </xsl:when>
@@ -363,6 +406,23 @@
            select="./*[1]"/>
      </xsl:for-each>
     </xsl:when>
+    
+    <xsl:when test="$name='inst'">
+     <xsl:apply-templates select="*[2]" mode="inline"/>
+     <FONT color="blue">{</FONT>
+     <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>
@@ -407,6 +467,15 @@
       </xsl:choose>
      </xsl:for-each>
     </xsl:when>
+    <!-- if then else -->
+    <xsl:when test="$name='ite'">
+     <xsl:text>if </xsl:text> 
+     <xsl:apply-templates select="*[2]"/>
+     <xsl:text> then </xsl:text>
+     <xsl:apply-templates select="*[3]"/>
+     <xsl:text> else </xsl:text>
+     <xsl:apply-templates select="*[4]"/>
+    </xsl:when>
     <!-- proof and side_proof -->
     <xsl:when test="$name='proof' or $name='side_proof'">
        <xsl:apply-templates mode="inline" select="*[position()=2]"/>
@@ -768,6 +837,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>
@@ -854,6 +927,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>
@@ -1074,6 +1203,29 @@
         <xsl:with-param name="current_indent" select="$current_indent+5"/>
        </xsl:apply-templates>
       </xsl:when>
+      <!-- it then else -->
+      <xsl:when test="$name='ite'">
+       <xsl:text>if </xsl:text> 
+       <xsl:apply-templates select="*[2]">
+        <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+       </xsl:apply-templates> 
+       <BR/> 
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <xsl:text> then </xsl:text>
+       <xsl:apply-templates select="*[3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 12"/>
+       </xsl:apply-templates>
+       <BR/> 
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <xsl:text> else </xsl:text>
+       <xsl:apply-templates select="*[4]">
+        <xsl:with-param name="current_indent" select="$current_indent + 12"/> 
+       </xsl:apply-templates>
+      </xsl:when>
 
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
@@ -1089,6 +1241,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
@@ -1112,7 +1282,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"/>');
@@ -1130,7 +1300,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..add3247b3 100644
--- a/helm/style/headercontent.xsl
+++ b/helm/style/headercontent.xsl
@@ -31,13 +31,17 @@
 
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
 
-<xsl:include href="contentlib.xsl"/>   <!-- FG -->
+<!-- Warning: the first included stylesheet has the lowest precedence -->
+<xsl:include href="contentlib.xsl"/>
 <xsl:include href="basic.xsl"/>
-<xsl:include href="arith.xsl"/>        <!-- FG -->
+<xsl:include href="arith.xsl"/>
 <xsl:include href="set.xsl"/>
+<xsl:include href="list.xsl"/>
 <xsl:include href="reals.xsl"/>
-<xsl:include href="ring.xsl"/>        <!-- FG -->
+<xsl:include href="ring.xsl"/>
 <xsl:include href="algebra.xsl"/> 
 <xsl:include href="lambda.xsl"/>
+<xsl:include href="positive.xsl"/>
+<xsl:include href="ccorn.xsl"/>
 
 </xsl:stylesheet>
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index 46fc61b24..91d978f5c 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -481,8 +481,6 @@
  </xsl:template>
 
 
-
-
 <!-- COUNTING -->
 
 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:neq
diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 83569d751..1d6dc4dd7 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,80 @@
                               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:variable name="uri">
+  <xsl:choose>
+   <xsl:when test="name(*[1])='CONST'">
+    <xsl:value-of select="*[1]/@uri"/>
+   </xsl:when>
+   <xsl:otherwise>
+    <!-- instantiate -->
+    <xsl:value-of select="*[1]/CONST[1]/@uri"/>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:variable>
+ <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="uri" select="$uri"/>
+      <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:template>
+
 
 <xsl:template mode="inductive" match="APPLY">
+ <xsl:param name="uri" select="''"/> 
  <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="$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 +126,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 +154,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 +178,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,28 +244,24 @@
      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="/.."/>
  <xsl:param name="bool_var" select="true()"/>
+ <!-- <xsl:value-of select="false()"/> -->
  <xsl:choose>
   <xsl:when test="count($arg_types) = 0">
     <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]/decl)"/>
+   <xsl:variable name="no_actual_abst_of_arg" 
+                 select="count($actual_args[1]/decl)"/> 
    <xsl:variable name="test_arg" 
-    select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/> 
+    select="($no_actual_abst_of_arg >= $no_expected_arg_of_arg)"/> 
    <xsl:call-template name="check_args">
     <xsl:with-param name="arg_types" select="$arg_types[position()>1]"/>
     <xsl:with-param name="actual_args" select="$actual_args[position()>1]"/>
@@ -208,25 +269,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 +290,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/ite.xsl b/helm/style/ite.xsl
new file mode 100644
index 000000000..1b0e14a72
--- /dev/null
+++ b/helm/style/ite.xsl
@@ -0,0 +1,48 @@
+<?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/.                                         -->
+
+<!--******************************************************************--> 
+<!-- If the else                                                      -->
+<!-- (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 match="MUTCASE[@uriType='cic:/Coq/Init/Datatypes/bool.ind']" mode="pure">
+    <m:apply helm:xref="{@id}">
+     <m:csymbol>ite</m:csymbol>
+     <xsl:apply-templates select="inductiveTerm/*[1]" mode="pure"/>
+     <xsl:apply-templates select="pattern/*[1]" mode="noannot"/>
+     <xsl:apply-templates select="pattern/*[2]" mode="noannot"/>
+    </m:apply>
+</xsl:template>
+
+</xsl:stylesheet>
+
+
diff --git a/helm/style/link.xsl b/helm/style/link.xsl
index e3568a18f..e6d639a3b 100644
--- a/helm/style/link.xsl
+++ b/helm/style/link.xsl
@@ -39,6 +39,8 @@
 
 <xsl:key name="id" use="@id" match="m:*"/>
 
+<xsl:param name="URLs_or_URIs" select="'URLs'"/>
+
 <xsl:template match = "m:semantics">
    <xsl:apply-templates select="*[1]" mode="semantics"/>
 </xsl:template>
@@ -52,7 +54,14 @@ xlink:href) -->
     <xsl:variable name="cnode" select="key('id',@xref)"/>
     <xsl:if test="$cnode/@definitionURL"> 
      <xsl:attribute name="xlink:href">
-      <xsl:call-template name="makeURL"><xsl:with-param name="uri" select="$cnode/@definitionURL"/></xsl:call-template>
+      <xsl:choose>
+       <xsl:when test="$URLs_or_URIs = 'URLs'">
+        <xsl:call-template name="makeURL"><xsl:with-param name="uri" select="$cnode/@definitionURL"/></xsl:call-template>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:value-of select="$cnode/@definitionURL"/> 
+       </xsl:otherwise>
+      </xsl:choose>
      </xsl:attribute>
     <!-- xlink:show='other' requires the exact modality to be -->
     <!-- specified in non-xlink markup. The point is that the -->
diff --git a/helm/style/logic.xsl b/helm/style/logic.xsl
new file mode 100644
index 000000000..0a261260a
--- /dev/null
+++ b/helm/style/logic.xsl
@@ -0,0 +1,155 @@
+<?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:choose>
+    <xsl:when test="count(*[5]/decl) = 2">
+     <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:apply-templates select="*[5]/*[3]" mode="lambda_prop"/>
+    </xsl:otherwise>
+   </xsl:choose> 
+  </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:choose>
+     <xsl:when test="count(*[5]/decl) > 2">
+      <xsl:apply-templates mode="lambda_prop" select="*[5]/decl[3]"/>
+     </xsl:when>
+     <xsl:otherwise>     
+      <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
+     </xsl:otherwise>
+    </xsl:choose>
+   </m:apply>
+</xsl:template>
+
+
+</xsl:stylesheet>
+
+
diff --git a/helm/style/mk_meta_and_dep_graph.xsl b/helm/style/mk_meta_and_dep_graph.xsl
index a9a9a954b..c860e4b46 100644
--- a/helm/style/mk_meta_and_dep_graph.xsl
+++ b/helm/style/mk_meta_and_dep_graph.xsl
@@ -24,16 +24,10 @@
 <!-- For details, see the HELM World-Wide-Web page,                    -->
 <!-- http://cs.unibo.it/helm/.                                         -->
 
-<!-- CSC: Sostituire l'andata a capo con la entity numerica opportuna -->
-<!DOCTYPE html [
- <!ENTITY CSCbr "
-">
-]>
-
 <xsl:stylesheet version="1.0"
   xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
   xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
-  xmlns:h="http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#">
+  xmlns:h="http://www.cs.unibo.it/helm/schemas/mattone.rdf#">
 
 <xsl:output method="text"/>
 
@@ -159,9 +153,9 @@
 
 <xsl:template match="/">
  <!--
- <xsl:text>strict digraph L0 { size = "83,83"; concentrate=true; node [style=filled, shape = box];&CSCbr;</xsl:text>
+ <xsl:text>strict digraph L0 { size = "83,83"; concentrate=true; node [style=filled, shape = box];&#x0A;</xsl:text>
  -->
- <xsl:text>strict digraph L0 { size = "83,83"; node [style=filled, shape = box];&CSCbr;</xsl:text>
+ <xsl:text>strict digraph L0 { size = "83,83"; node [style=filled, shape = box];&#x0A;</xsl:text>
  <xsl:variable name="quoted_CICURI">
   <xsl:call-template name="quote_url">
    <xsl:with-param name="s" select="$CICURI"/>
@@ -239,7 +233,7 @@
  <xsl:if test="name(document(concat($uri_set_queueURL,'is_overflowed?uri=',$quotedCurrentCICURI,'&amp;nonce=',generate-id(),'&amp;PID=',$PID))/*)='true'">
   <xsl:text>,color=red</xsl:text>
  </xsl:if>
- <xsl:text>];&CSCbr;</xsl:text>
+ <xsl:text>];&#x0A;</xsl:text>
 </xsl:template>
 
 <xsl:template match="*">
@@ -248,12 +242,12 @@
  <xsl:for-each select="*/*/*">
   <xsl:variable name="quotedURI">
    <xsl:call-template name="quote">
-    <xsl:with-param name="s" select="@rdf:value"/>
+    <xsl:with-param name="s" select="h:occurrence"/>
    </xsl:call-template>
   </xsl:variable>
   <xsl:variable name="quoted_uri">
    <xsl:call-template name="quote_url">
-    <xsl:with-param name="s" select="@rdf:value"/>
+    <xsl:with-param name="s" select="h:occurrence"/>
    </xsl:call-template>
   </xsl:variable>
   <!-- The nonce, quotedCurrentCICURI are used to force the document reload -->
@@ -263,7 +257,7 @@
    <xsl:text> -&gt; </xsl:text>
    <xsl:value-of select="$quotedURI"/>
    <xsl:value-of select="$link_direction"/>
-   <xsl:text>;&CSCbr;</xsl:text>
+   <xsl:text>;&#x0A;</xsl:text>
   </xsl:if>
  </xsl:for-each>
 </xsl:template>
diff --git a/helm/style/mk_meta_theory.xsl b/helm/style/mk_meta_theory.xsl
index 3a07962a9..e433c4b26 100644
--- a/helm/style/mk_meta_theory.xsl
+++ b/helm/style/mk_meta_theory.xsl
@@ -28,25 +28,19 @@
    xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
    xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
-   xmlns:h="http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#">
-
-<xsl:variable name="MainConclusion" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#MainConclusion'"/>
-<xsl:variable name="InConclusion" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#InConclusion'"/>
-<xsl:variable name="MainHypothesis" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#MainHypothesis'"/>
-<xsl:variable name="InHypothesis" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#InHypothesis'"/>
-<xsl:variable name="InBody" select="'http://www.cs.unibo.it/helm/schemas/schema-h.rdf#InBody'"/>
+   xmlns:h="http://www.cs.unibo.it/helm/schemas/mattone.rdf#">
 
 <xsl:template match="/">
                <html> 
                 <head>
-                 <title>Occurrences of <xsl:value-of select="*/*/@rdf:value"/></title>
+                 <title>Occurrences of <xsl:value-of select="*/*/@rdf:about"/></title>
                  <style>
                   a { text-decoration: none }
                   a.underline {text-decoration: underline }
                  </style>
                 </head>
                 <!-- CSC: method onLoad to be removed once the window -->
-                <!-- CSC: becomes a frame                              -->
+                <!-- CSC: becomes a frame                             -->
                 <body bgcolor="white" onLoad="window.focus()">
                 <xsl:apply-templates/>
                 </body>
@@ -55,15 +49,15 @@
 
 <xsl:template match="h:Object">
  <xsl:variable name="no_main"
-   select="count(*/h:Occurrence[@rdf:about=$MainConclusion])"/>
+   select="count(*/h:Occurrence/h:position[text()='MainConclusion'])"/>
  <xsl:variable name="no_concl"
-   select="count(*/h:Occurrence[@rdf:about=$InConclusion])"/>
+   select="count(*/h:Occurrence/h:position[text()='InConclusion'])"/>
  <xsl:variable name="no_main_hyp"
-   select="count(*/h:Occurrence[@rdf:about=$MainHypothesis])"/>
+   select="count(*/h:Occurrence/h:position[text()='MainHypothesis'])"/>
  <xsl:variable name="no_in_hyp"
-   select="count(*/h:Occurrence[@rdf:about=$InHypothesis])"/>
+   select="count(*/h:Occurrence/h:position[text()='InHypothesis'])"/>
  <xsl:variable name="no_body"
-   select="count(*/h:Occurrence[@rdf:about=$InBody])"/>
+   select="count(*/h:Occurrence/h:position[text()='InBody'])"/>
  <h1>Occurrences of <xsl:value-of select="@rdf:about"/></h1>
  
  <ul>
@@ -92,17 +86,17 @@
   <xsl:when test="$no_main = 0"/>
   <xsl:when test="15 > $no_main">
    <h2><a name="main">Head position inside conclusion:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainConclusion]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='MainConclusion']">
     <div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
     </div>
    </xsl:for-each>
   </xsl:when>
   <xsl:when test="$no_main >= 15">
    <h2><a name="main">Head position inside conclusion:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainConclusion]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='MainConclusion']">
     <div style="margin: 0cm 0cm 0cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
     </div>
    </xsl:for-each>
   </xsl:when>
@@ -111,17 +105,17 @@
   <xsl:when test="$no_concl = 0"/>
   <xsl:when test="15 > $no_concl">
    <h2><a name="concl">Inside conclusion:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$InConclusion]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='InConclusion']">
     <div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
     </div>
    </xsl:for-each>
   </xsl:when>
   <xsl:when test="$no_concl >= 15">
    <h2><a name="concl">Inside conclusion:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$InConclusion]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='InConclusion']">
     <div style="margin: 0cm 0cm 0cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
     </div>
    </xsl:for-each>
   </xsl:when>
@@ -130,17 +124,17 @@
   <xsl:when test="$no_main_hyp = 0"/>
   <xsl:when test="15 > $no_main_hyp">
    <h2><a name="main_hyp">Head position inside an hypothesis:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainHypothesis]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='MainHypothesis']">
     <div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
     </div>
    </xsl:for-each>
   </xsl:when>
   <xsl:when test="$no_main_hyp >= 15">
    <h2><a name="main_hyp">Head position inside an hypothesis:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$MainHypothesis]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='MainHypothesis']">
     <div style="margin: 0cm 0cm 0cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
     </div>
    </xsl:for-each>
   </xsl:when> 
@@ -149,26 +143,26 @@
   <xsl:when test="$no_in_hyp = 0"/>
   <xsl:when test="15 > $no_in_hyp">
    <h2><a name="hyp">Inside an hypothesis:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$InHypothesis]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='InHypothesis']">
     <div style="margin: 0.25cm 0cm 0.25cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="typeonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="typeonly"/>
     </div>
    </xsl:for-each>
   </xsl:when>
   <xsl:when test="$no_in_hyp >= 15">
    <h2><a name="hyp">Inside an hypothesis:</a></h2>
-   <xsl:for-each select="*/h:Occurrence[@rdf:about=$InHypothesis]">
+   <xsl:for-each select="*/h:Occurrence[h:position/text()='InHypothesis']">
     <div style="margin: 0cm 0cm 0cm 0.75cm">
-     <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+     <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
     </div>
    </xsl:for-each>
   </xsl:when>
  </xsl:choose>
  <xsl:if test="$no_body > 0">
   <h2><a name="body">Inside the body:</a></h2>
-  <xsl:for-each select="*/h:Occurrence[@rdf:about=$InBody]">
+  <xsl:for-each select="*/h:Occurrence[h:position/text()='InBody']">
    <div style="margin: 0cm 0cm 0cm 0.75cm">
-    <ht:OBJECT uri="{@rdf:value}" mode="linkonly"/>
+    <ht:OBJECT uri="{h:occurrence}" mode="linkonly"/>
    </div>
   </xsl:for-each>
  </xsl:if>
diff --git a/helm/style/mmlctop.xsl b/helm/style/mmlctop.xsl
index 554c3a87b..b63ebee8a 100644
--- a/helm/style/mmlctop.xsl
+++ b/helm/style/mmlctop.xsl
@@ -1293,18 +1293,38 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
   <xsl:choose>
     <xsl:when test="$IN_PREC &gt; $MINUS_PREC or $IN_PREC=$MINUS_PREC and
                                                         $PARAM=$PAR_SAME">
-      <m:mfenced separators="">
-        <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
-          <xsl:attribute name="xref">
-            <xsl:value-of select="@id"/>
-          </xsl:attribute>
-        </xsl:if>
-        <xsl:apply-templates select="." mode="minus">
-          <xsl:with-param name="PARAM" select="$PARAM"/>
-          <xsl:with-param name="PAREN" select="$PAR_YES"/>
-          <xsl:with-param name="PAR_NO_IGNORE" select="$PAR_NO_IGNORE"/>
-        </xsl:apply-templates>
-      </m:mfenced>
+      <!-- HELM: m:mrow is now used when the minus operator is unary.
+           Igor used m:mfenced instead. -->
+      <xsl:choose>
+       <xsl:when test="count(*)=2">
+        <m:mrow>
+          <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
+            <xsl:attribute name="xref">
+              <xsl:value-of select="@id"/>
+            </xsl:attribute>
+          </xsl:if>
+          <xsl:apply-templates select="." mode="minus">
+            <xsl:with-param name="PARAM" select="$PARAM"/>
+            <xsl:with-param name="PAREN" select="$PAR_YES"/>
+            <xsl:with-param name="PAR_NO_IGNORE" select="$PAR_NO_IGNORE"/>
+          </xsl:apply-templates>
+        </m:mrow>
+       </xsl:when>
+       <xsl:otherwise>
+        <m:mfenced separators="">
+          <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
+            <xsl:attribute name="xref">
+              <xsl:value-of select="@id"/>
+            </xsl:attribute>
+          </xsl:if>
+          <xsl:apply-templates select="." mode="minus">
+            <xsl:with-param name="PARAM" select="$PARAM"/>
+            <xsl:with-param name="PAREN" select="$PAR_YES"/>
+            <xsl:with-param name="PAR_NO_IGNORE" select="$PAR_NO_IGNORE"/>
+          </xsl:apply-templates>
+        </m:mfenced>
+       </xsl:otherwise>
+      </xsl:choose>
     </xsl:when>
     <xsl:when test="$IN_PREC &gt; $NO_PREC and $IN_PREC &lt; $FUNCTION_PREC
                     and not($SEM_SW=$SEM_ALL) and not($SEM_SW=$SEM_XREF)
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 4a801a654..fad3dce6b 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1105,6 +1105,96 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- INST -->
+      <xsl:when test="$name='inst'">
+       <m:mrow>
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo stretchy="false">{</m:mo>
+        <xsl:for-each select="*[(position()>2) and (position() mod 2 = 1)]">
+         <xsl:apply-templates select="."/>
+         <m:mo stretchy="false">:=</m:mo>
+         <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+        </xsl:for-each>
+        <m:mo stretchy="false">}</m:mo>
+       </m:mrow>
+      </xsl:when>
+      <!-- APPEND -->
+      <xsl:when test="$name='append'">
+       <xsl:choose>
+        <xsl:when test="$charlength >= $framewidth">
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <xsl:apply-templates select="*[2]"/>
+             <m:mo>@</m:mo>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <xsl:apply-templates select="*[3]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:mrow>
+          <xsl:apply-templates select="*[2]"/>
+          <m:mo>@</m:mo>
+          <xsl:apply-templates select="*[3]"/>
+         </m:mrow>
+        </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <!-- ITE -->
+      <xsl:when test="$name='ite'">
+       <xsl:choose>
+        <xsl:when test="$charlength >= $framewidth">
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>if</m:mo>
+             <xsl:apply-templates select="*[2]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>then</m:mo>
+             <xsl:apply-templates select="*[3]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mo>else</m:mo>
+             <xsl:apply-templates select="*[4]"/>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
+        </xsl:when>
+        <xsl:otherwise>
+         <m:mrow>
+          <m:mo>if</m:mo>
+          <xsl:apply-templates select="*[2]"/>
+          <m:mo>then</m:mo>
+          <xsl:apply-templates select="*[3]"/>
+          <m:mo>else</m:mo>
+          <xsl:apply-templates select="*[4]"/>
+         </m:mrow>
+        </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
       <!-- ***************************************** -->
@@ -1478,23 +1568,112 @@ which generates the toplevel element (see for instance xlink) -->
            </m:mrow>
           </m:mtd>
          </m:mtr>
-         <m:mtr>
-          <m:mtd>
-           <m:mrow>
-            <m:mtext>Rewrite</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[3]"/>
-	    <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-	    <m:mtext>with</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[4]"/>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>by</m:mtext>
-            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[5]"/>
-           </m:mrow>
-          </m:mtd>
-         </m:mtr>
+         <xsl:variable name="charlength1">
+          <xsl:apply-templates select="*[3]" mode="root_charcount"/>
+         </xsl:variable>
+         <xsl:variable name="charlength2">
+          <xsl:apply-templates select="*[4]" mode="root_charcount"/>
+         </xsl:variable>
+         <xsl:variable name="charlength3">
+          <xsl:apply-templates select="*[5]" mode="root_charcount"/>
+         </xsl:variable>
+         <xsl:variable name="split1"
+           select="($charlength1 + $charlength2) >= $framewidth"/>
+         <xsl:variable name="split2"
+           select="($charlength2 + $charlength3) >= $framewidth"/>
+         <xsl:choose>
+          <xsl:when test="$split1">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>Rewrite</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[3]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+           <xsl:choose>
+            <xsl:when test="$split2">
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+	        <m:mtext>with</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[4]"/>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+                <m:mtext>by</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[5]"/>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+            </xsl:when>
+            <xsl:otherwise>
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+	        <m:mtext>with</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[4]"/>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <m:mtext>by</m:mtext>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:apply-templates select="*[5]"/>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+            </xsl:otherwise>
+           </xsl:choose>
+          </xsl:when>
+          <xsl:when test="$split2">
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>Rewrite</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[3]"/>
+	      <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+	      <m:mtext>with</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[4]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>by</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[5]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:when>
+          <xsl:otherwise>
+           <m:mtr>
+            <m:mtd>
+             <m:mrow>
+              <m:mtext>Rewrite</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[3]"/>
+	      <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+	      <m:mtext>with</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[4]"/>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <m:mtext>by</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[5]"/>
+             </m:mrow>
+            </m:mtd>
+           </m:mtr>
+          </xsl:otherwise>
+         </xsl:choose>
         </m:mtable>
       </xsl:when>
       <!-- not existing any more
@@ -1966,7 +2145,7 @@ which generates the toplevel element (see for instance xlink) -->
         <xsl:apply-templates select="*[3]"/>
       </xsl:when>
       <!-- interp -->
-      <xsl:when test="$name='forgetful'">
+      <xsl:when test="$name='interp'">
        <m:mfenced open="[" close="]">
         <xsl:if test="$id != ''">
          <xsl:attribute name="xref"><xsl:value-of select="$id"/></xsl:attribute>
@@ -1977,7 +2156,7 @@ which generates the toplevel element (see for instance xlink) -->
 
       <!-- ERROR -->
       <xsl:otherwise>
-       <m:mi>ERROR</m:mi>
+       <m:mi>ERROR(&quot;<xsl:value-of select="$name"/>&quot;)</m:mi>
       </xsl:otherwise>
      </xsl:choose>
     </m:mrow>
@@ -2086,6 +2265,24 @@ which generates the toplevel element (see for instance xlink) -->
 <!--       COUNTING       -->
 <!--**********************-->
 
+<!-- enter this counting mode selecting the root -->
+<xsl:template match="*" mode="root_charcount">
+<xsl:param name="incurrent_length" select="0"/>
+ <xsl:choose>
+  <xsl:when test="count(*)=0">
+   <xsl:value-of select="0"/>
+  </xsl:when>
+  <xsl:when test="name()='m:ci'">
+   <xsl:value-of select="string-length()"/>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:apply-templates select="*[1]" mode="charcount">
+    <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
+   </xsl:apply-templates>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
 <xsl:template match="m:cn|m:and|m:or|m:not|m:exists|m:eq|m:lt|m:leq|m:gt|m:geq
  |m:in|m:notin|m:intersect|m:union|m:subset|m:prsubset|m:card|m:setdiff
  |m:plus|m:minus|m:times" mode="charcount">
@@ -2113,14 +2310,24 @@ which generates the toplevel element (see for instance xlink) -->
 </xsl:template>
 
 <xsl:template match="m:ci|m:csymbol" mode="charcount">
-<xsl:param name="incurrent_length" select="0"/> 
-<xsl:param name="nosibling" select="0"/>
+ <xsl:param name="incurrent_length" select="0"/> 
+ <xsl:param name="nosibling" select="0"/>
+ <xsl:variable name="mylength">
+  <xsl:choose>
+   <!-- special notation -->
+   <xsl:when test="text()='append'">3</xsl:when>
+   <!-- no notation -->
+   <xsl:otherwise>
+    <xsl:value-of select="string-length()"/>
+   </xsl:otherwise>
+  </xsl:choose>
+ </xsl:variable>
     <xsl:choose>
-    <xsl:when test="$framewidth > ($incurrent_length + string-length()) and ($nosibling = 0)">
-     <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
+    <xsl:when test="$framewidth > ($incurrent_length + $mylength) and ($nosibling = 0)">
+     <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + $mylength"/></xsl:apply-templates></xsl:variable>
      <xsl:choose>
      <xsl:when test="string($siblength) = &quot;&quot;">
-      <xsl:value-of select="$incurrent_length + string-length()"/>
+      <xsl:value-of select="$incurrent_length + $mylength"/>
      </xsl:when>
      <xsl:otherwise>
       <xsl:value-of select="number($siblength)"/>
@@ -2128,7 +2335,7 @@ which generates the toplevel element (see for instance xlink) -->
      </xsl:choose>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:value-of select="$incurrent_length + string-length()"/>
+     <xsl:value-of select="$incurrent_length + $mylength"/>
     </xsl:otherwise>
     </xsl:choose>
 </xsl:template> 
diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl
index 5cf944e72..7081ad83f 100644
--- a/helm/style/mmlnotation.xsl
+++ b/helm/style/mmlnotation.xsl
@@ -139,26 +139,24 @@
      <m:mtd>
       <m:mrow>
        <m:mo stretchy="false">(</m:mo>
-       <xsl:apply-templates select="*[position()=2]"/>
+       <xsl:apply-templates select="*[2]"/>
+      </m:mrow>
+     </m:mtd>
+    </m:mtr>
+    <m:mtr>
+     <m:mtd>
+      <m:mrow>
+       <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+       <m:mo>
+        <xsl:if test="*[1]/@id">
+         <xsl:attribute name="xref">
+          <xsl:value-of select="*[1]/@id"/>
+         </xsl:attribute>
+        </xsl:if><xsl:value-of select="$symbol"/></m:mo>
+       <xsl:apply-templates select="*[3]"/>
       </m:mrow>
      </m:mtd>
     </m:mtr>
-    <xsl:for-each select = "*[position()>2]">
-     <m:mtr>
-      <m:mtd>
-       <m:mrow>
-        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-        <m:mo>
-         <xsl:if test="*[1]/@id">
-          <xsl:attribute name="xref">
-           <xsl:value-of select="*[1]/@id"/>
-          </xsl:attribute>
-         </xsl:if><xsl:value-of select="$symbol"/></m:mo>
-        <xsl:apply-templates select="."/>
-       </m:mrow>
-      </m:mtd>
-     </m:mtr>
-    </xsl:for-each>
     <m:mtr>
      <m:mtd>
       <m:mrow>
@@ -396,4 +394,4 @@
 </xsl:template>
 
 
-</xsl:stylesheet>
\ No newline at end of file
+</xsl:stylesheet>
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index ceb7a22ba..5b243e783 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -52,6 +52,51 @@
     <xsl:apply-templates select="*[1]"/>
 </xsl:template>
 
+
+<!-- FUNZIONI AUSILIARIE -->
+
+<xsl:template name="name_of_uri_bis">
+ <xsl:param name="uri" select="&quot;&quot;"/>
+  <xsl:variable name="suffix" select="substring-after($uri, &quot;/&quot;)"/>
+  <xsl:choose>
+   <xsl:when test="$suffix = &quot;&quot;">
+    <xsl:value-of select="substring-before($uri,&quot;.var&quot;)"/>
+   </xsl:when>
+   <xsl:otherwise>
+    <xsl:call-template name="name_of_uri_bis">
+     <xsl:with-param name="uri" select="$suffix"/>
+    </xsl:call-template>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+<xsl:template name="var_name">
+ <xsl:param name="uri"/>
+ <xsl:param name="string" select="&quot;&quot;"/>
+  <xsl:variable name="prefix0" select="substring-before($uri, &quot; &quot;)"/>
+  <xsl:variable name="suffix" select="substring-after($uri, &quot; &quot;)"/> 
+  <xsl:variable name="prefix">
+   <xsl:call-template name="name_of_uri_bis">
+    <xsl:with-param name="uri" select="$prefix0"/>
+   </xsl:call-template>
+  </xsl:variable> 
+  <!--xsl:if test="string($prefix) != &quot; &quot; "-->
+   <xsl:variable name="string1" select="concat($string,', ', $prefix)"/>
+  <!--/xsl:if-->
+  <xsl:choose>
+   <xsl:when test="$suffix = &quot;&quot;">
+   <xsl:value-of select="substring-after(concat($string1, ' '),',')"/>
+   </xsl:when>
+   <xsl:otherwise>
+   <xsl:call-template name="var_name">
+    <xsl:with-param name="uri" select="$suffix"/>
+    <xsl:with-param name="string" select="$string1"/>
+   </xsl:call-template>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+				  
+				  
 <!-- CIC OBJECTS -->
 
 <xsl:template match="Sequent">  <!-- For Sequents there are no annotations --> 
@@ -73,11 +118,15 @@
     </Sequent> 
 </xsl:template>
 
-<xsl:template match="Definition" mode="noannot">
+<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>
-       <xsl:value-of select="@params"/>
+      <xsl:call-template name="var_name">
+       <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+      </xsl:call-template>
       </Params>
      </xsl:if>
 <!--     <xsl:choose>
@@ -93,29 +142,35 @@
       </xsl:otherwise>
      </xsl:choose> -->
      <body>
-      <xsl:apply-templates select="body/*[1]"/>
+      <m:ci definitionURL="{$ConstantBodyUrl}">click here</m:ci>
      </body>
      <type>
-       <xsl:apply-templates select="type/*[1]"/>
+       <xsl:apply-templates select="./*[1]"/>
      </type>
     </Definition> 
 </xsl:template>
 
-<xsl:template match="Axiom" mode="noannot"> 
-    <Axiom name="{@name}" helm:xref="{@id}">
+<xsl:template match="ConstantBody" mode= "noannot">
+    <Definition name="{@for}" helm:xref="{@id}">  
      <xsl:if test="string(@params) != &quot;&quot;">
       <Params>
-       <xsl:value-of select="@params"/>
+       <xsl:call-template name="var_name">
+       <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+       </xsl:call-template>
       </Params>
      </xsl:if>
+     <body>
+      <xsl:apply-templates select="./*[1]"/>
+     </body>
      <type>
-       <xsl:apply-templates select="type/*[1]"/>
+       <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
      </type>
-    </Axiom> 
+    </Definition>
 </xsl:template>
 
+
 <xsl:template match="CurrentProof" mode="noannot">
-    <CurrentProof name="{@name}" helm:xref="{@id}">
+    <CurrentProof name="{@of}" helm:xref="{@id}">
      <xsl:for-each select="Conjecture">
       <Conjecture no="{@no}" helm:xref="{@id}">
         <xsl:for-each select="*">
@@ -133,7 +188,7 @@
        <xsl:apply-templates select="body/*[1]"/>
      </body>
      <type>
-       <xsl:apply-templates select="type/*[1]"/>
+       <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
      </type>
     </CurrentProof> 
 </xsl:template>
diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl
index 7d890d611..5bad7e108 100644
--- a/helm/style/objtheorycontent.xsl
+++ b/helm/style/objtheorycontent.xsl
@@ -43,42 +43,42 @@
 
 <!-- CIC DEFINITION -->
 
-<xsl:template match="Definition">
-    <xsl:choose>
+<xsl:template match="ConstantType">
+  <xsl:choose>
    <xsl:when test="$type='typeonly'">
     <type>
-     <xsl:apply-templates select="type/*[1]"/>
+     <xsl:apply-templates select="./*[1]" mode="noannot"/>
     </type>
    </xsl:when>
    <xsl:otherwise>
     <Definition name="{@name}" helm:xref="{@id}">  
      <xsl:if test="string(@params) != &quot;&quot;">
       <Params>
-       <xsl:value-of select="@params"/>
+       <xsl:call-template name="var_name">
+        <xsl:with-param name="uri" select="concat(@params, ' ')"/>
+       </xsl:call-template>
       </Params>
      </xsl:if>
-     <body>
-       <xsl:apply-templates select="body/*[1]"/>
-     </body>
+     <body/>
      <type>
-       <xsl:apply-templates select="type/*[1]"/>
+       <xsl:apply-templates select="./*[1]" mode="noannot"/>
      </type>
     </Definition>
    </xsl:otherwise>
-   </xsl:choose>
+  </xsl:choose>
 </xsl:template>
 
 <xsl:template match="Axiom|CurrentProof|InductiveDefinition|Variable">
     <xsl:apply-templates select="." mode="noannot"/>
 </xsl:template>
 
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate">
     <m:math>
      <xsl:apply-templates select="." mode="noannot"/>
     </m:math>
 </xsl:template>
 
-<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate" mode="noannot">
     <xsl:apply-templates select="." mode="pure"/>
 </xsl:template>
 
diff --git a/helm/style/params.xsl b/helm/style/params.xsl
index d703bfe06..1b5f41670 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"/>
@@ -163,14 +184,11 @@
       </xsl:call-template>
      </xsl:variable>
      <xsl:choose>
-	  <xsl:when test="$offset > 0">
-	   <xsl:variable name="params"> 
-        <xsl:variable name="second_url">
-			<xsl:call-template name="URLofURI4getter">
-				<xsl:with-param name="uri" select="$second_uri"/>
-			</xsl:call-template>
-		</xsl:variable>
-        <xsl:value-of select="document($second_url)/*/@params"/>
+      <xsl:when test="$offset > 0">
+       <xsl:variable name="params"> 
+        <xsl:variable name="second_url"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$second_uri"/></xsl:call-template></xsl:variable>
+        <xsl:value-of 
+            select="document($second_url)/*/@params"/>
        </xsl:variable>
        <xsl:variable name="minimum">
         <xsl:call-template name="min">
@@ -179,7 +197,9 @@
         </xsl:call-template>
        </xsl:variable>
        <xsl:choose>
-        <xsl:when test="0 > $minimum">0</xsl:when>
+        <xsl:when test="0 > $minimum">
+         0
+        </xsl:when>
         <xsl:otherwise>
          <xsl:variable name="relevant_params">
           <!-- the blank after : in the next line is essential -->
@@ -198,11 +218,13 @@
            <xsl:with-param name="counter" select="0"/>
           </xsl:call-template>
          </xsl:variable>
-         <xsl:value-of select="number($tokens - $separators)"/>
+         <xsl:value-of select="$tokens - $separators"/>
         </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
-      <xsl:otherwise>0</xsl:otherwise>
+      <xsl:otherwise>
+      0
+      </xsl:otherwise>
      </xsl:choose>
 </xsl:template>
 
@@ -275,25 +297,59 @@
     <xsl:when test="($noparams != 0) and ((name(.)=string($binder)) or (name(.)=&quot;CAST&quot;))">
      <xsl:choose>
      <xsl:when test="name(.) = string($binder)">
-      <xsl:if test="$target = 0">
-       <xsl:choose>
-       <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
-        <m:ci>
-         <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
-        </m:ci>
+      <xsl:choose>
+       <xsl:when test="$noparams >= count(decl)">
+        <xsl:for-each select="decl">
+         <xsl:if test="$target = 0">
+          <xsl:choose>
+          <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
+           <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>
+          </xsl:when>
+          <xsl:otherwise> 
+           <Param name="{@binder}">
+            <xsl:apply-templates select="*[1]"/>
+           </Param>
+          </xsl:otherwise>
+          </xsl:choose>
+         </xsl:if> 
+	</xsl:for-each>
+        <xsl:apply-templates select="target/*[1]" mode="abstparams">
+         <xsl:with-param name="noparams" select="$noparams - count(decl)"/>
+         <xsl:with-param name="target" select="$target"/>
+         <xsl:with-param name="binder" select="$binder"/>
+        </xsl:apply-templates>
        </xsl:when>
-       <xsl:otherwise> 
-        <Param name="{target/@binder}">
-         <xsl:apply-templates select="source"/>
-        </Param>
+       <xsl:otherwise>
+        <xsl:for-each select="decl[$noparams >= position()]">
+         <xsl:if test="$target = 0">
+          <xsl:choose>
+          <xsl:when test="string($binder) = &quot;LAMBDA&quot;">
+           <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>
+          </xsl:when>
+          <xsl:otherwise> 
+           <Param name="{@binder}">
+            <xsl:apply-templates select="*[1]"/>
+           </Param>
+          </xsl:otherwise>
+          </xsl:choose>
+         </xsl:if> 
+	</xsl:for-each>
+        <xsl:if test="$target = 1">
+         <xsl:choose>
+	  <xsl:when test="name(.)=&quot;PROD&quot;">
+	   <xsl:apply-templates select="decl[position()=$noparams+1]" mode="prod"/>
+	  </xsl:when>
+	  <xsl:otherwise>
+	   <xsl:apply-templates select="decl[position()=$noparams+1]" mode="lambda_prop"/>
+	  </xsl:otherwise>
+	 </xsl:choose>
+        </xsl:if>
        </xsl:otherwise>
-       </xsl:choose>
-      </xsl:if>
-      <xsl:apply-templates select="target/*[1]" mode="abstparams">
-       <xsl:with-param name="noparams" select="$noparams - 1"/>
-       <xsl:with-param name="target" select="$target"/>
-       <xsl:with-param name="binder" select="$binder"/>
-      </xsl:apply-templates>
+      </xsl:choose>
      </xsl:when>
      <xsl:otherwise>
       <xsl:apply-templates select="term/*[1]" mode="abstparams">
@@ -356,7 +412,7 @@
  <xsl:when test="name(.) = &quot;PROD&quot;">
   <xsl:apply-templates select="target/*[1]" mode="counting">
    <xsl:with-param name="noparams" select="$noparams"/>
-   <xsl:with-param name="count" select="$count + 1"/>
+   <xsl:with-param name="count" select="$count + count(decl)"/> 
   </xsl:apply-templates>
  </xsl:when>
  <xsl:when test="name(.) = &quot;CAST&quot;">
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index f61cbe6d9..dbcfabaa3 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -34,15 +34,19 @@
                               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 -->
 
-<!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
 <xsl:key name="typeid" use="@of" match="TYPE"/>
 
-<!-- ALL this elements does not have inner type -->
-<xsl:template match="PROD|SORT|MUTIND" mode="noannot">
+<!-- These elements do not have inner type -->
+<xsl:template match="PROD|SORT|MUTIND|instantiate" mode="noannot">
  <xsl:apply-templates select="." mode="pure"/>
 </xsl:template>
 
@@ -59,10 +63,10 @@
  </xsl:variable>
  <xsl:choose>
   <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
+   <!--xsl:when test="@sort='Prop'"-->
    <m:apply helm:xref="{@id}">
     <m:csymbol>proof</m:csymbol>
     <xsl:apply-templates mode="proof_transform" select="."/>
-    <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
     <xsl:for-each select="$InnerTypes">
      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
     </xsl:for-each>
@@ -76,8 +80,19 @@
 
 <!-- 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: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">
@@ -87,30 +102,114 @@
   </xsl:for-each>
  </xsl:variable>
  <xsl:choose>
-  <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
+  <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>
+
+<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 $innertype_available='yes'">
+   <m:apply helm:xref="{@id}">
+    <m:csymbol>proof</m:csymbol>
+    <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>
+   <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>
 
+<xsl:template match="target" mode="letin_prop">
+ <xsl:apply-templates select="*[1]" mode="noannot"/>
+</xsl:template>
+
 <!-- ALL these elements have inner type -->
-<xsl:template match="LETIN|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
+<xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
  <xsl:variable name="id" select="@id"/>
  <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:apply-templates mode="try_inductive" select="."/> -->
     <xsl:for-each select="$InnerTypes">
      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
     </xsl:for-each>
@@ -132,588 +231,32 @@
  </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>
-
-<xsl:template mode="eq_transitive" match="*">
- <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
- <xsl:choose>
-  <xsl:when test="name()='APPLY'">
-   <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
-   <xsl:variable name="id" select="@id"/>
-   <xsl:choose>
-    <!-- ricordarsi di trattare il parametro -->
-    <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
-     <!-- <m:ci>eccomi-3</m:ci> -->
-     <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
-     <xsl:apply-templates mode="noannot" select="*[4]"/>
-     <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
-    </xsl:when>
-    <xsl:otherwise>
-     <xsl:call-template name="generate_side_proof">
-      <xsl:with-param name="proof" select="."/>
-      <xsl:with-param name="show_statement" select="0"/>
-     </xsl:call-template> 
-    </xsl:otherwise>
-   </xsl:choose>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:call-template name="generate_side_proof">
-    <xsl:with-param name="proof" select="."/>
-    <xsl:with-param name="show_statement" select="0"/>
-   </xsl:call-template>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<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/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">
-       <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/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">
-       <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: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>
-
 <xsl:template mode="proof_transform" match="*">
  <xsl:choose>
   <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/CSetoids/CSetoid_basics/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/COrdField_axioms/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/COrdFields/COrdField_axioms/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/COrdFields/COrdField_axioms/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/Equality/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/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/Equality/eq_ind.con' or
- attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/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/Conjunction/and_ind.con'] 
- and count(child::*) = 6 
- and name(*[5])='LAMBDA' 
- and name(*[5]/target/*[1])='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]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
-       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
-       <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/> 
-      </m:apply>
-    </xsl:when>
-    <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Logic/Disjunction/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/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]/target/@binder"/>
-           </m:ci>
-           <m:type>
-            <xsl:apply-templates mode="pure" select="*[5]/source/*[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]/target/@binder"/>
-           </m:ci>
-           <m:type>
-            <xsl:apply-templates mode="pure" select="*[6]/source/*[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/First_order_quantifiers/ex_ind.con'])  
- and count(child::*) = 6 
- and name(*[5])='LAMBDA' 
- and name(*[5]/target/*[1])='LAMBDA'"> 
-      <m:apply helm:xref="{@id}">
-       <m:csymbol>ex_ind</m:csymbol>
-       <xsl:apply-templates mode="noannot" select="*[6]"/>
-       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
-       <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
-       <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
-       <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
-      </m:apply>
-    </xsl:when>
-    <xsl:when test="name(*[1])='CONST'">
+    <xsl:when test="name(*[1])='CONST' or 
+      (name(*[1])='instantiate' and name(*[1]/*[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">
-          <xsl:value-of select="*[1]/target/@binder"/>
+          <xsl:value-of select="*[1]/*[1]/@binder"/>
          </xsl:with-param>
         </xsl:call-template>
        </m:ci>
-       <xsl:apply-templates mode="noannot" select="*[2]"/>
-      </m:apply>
-      <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
+      </m:bvar>
+      <xsl:apply-templates mode="noannot" select="*[2]"/>
+      <xsl:apply-templates mode="lambda_prop" select="*[1]/*[2]"/>
      </m:apply>
     </xsl:when>
     <xsl:otherwise>
@@ -721,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>
@@ -876,6 +393,49 @@
    </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="@sort='Prop' and (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"/>
@@ -896,11 +456,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>
@@ -926,7 +487,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>
@@ -960,7 +522,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>
@@ -993,27 +555,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/ring.xsl b/helm/style/ring.xsl
index d57723ea8..5136e77d5 100644
--- a/helm/style/ring.xsl
+++ b/helm/style/ring.xsl
@@ -4,12 +4,12 @@
                               xmlns:m="http://www.w3.org/1998/Math/MathML"
                               xmlns:helm="http://www.cs.unibo.it/helm">
 			      
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con']" mode="pure">
+<xsl:template match="APPLY[CONST[@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con']] | APPLY[instantiate/CONST[@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con']]" mode="proof_transform">
    <xsl:choose>
-      <xsl:when test="count(child::*) > 1">
+      <xsl:when test="count(child::*) = 2">
          <m:apply helm:xref="{@id}">
             <m:csymbol>app</m:csymbol>
-            <xsl:apply-templates mode="noannot" select="*[1]"/>
+            <xsl:apply-templates mode="noannot" select="*[1]/*[1]"/>
             <m:ci>...</m:ci>
          </m:apply>
       </xsl:when>
@@ -19,12 +19,12 @@
    </xsl:choose>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con']" mode="pure">
+<xsl:template match="APPLY[instantiate/CONST[@uri='cic:/Coq/ring/Ring_abstract/interp_ap.con']] | APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_ap.con']" mode="pure">
    <xsl:choose>
-      <xsl:when test="count(child::*) = 9">
+      <xsl:when test="count(child::*) = 2">
          <xsl:call-template name="start-interp">
-	    <xsl:with-param name="rtree" select="*[9]"/>
-            <xsl:with-param name="atree" select="*[8]"/>
+	    <xsl:with-param name="rtree" select="*[2]"/>
+            <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
 	 </xsl:call-template>
       </xsl:when>
       <xsl:otherwise>
@@ -33,16 +33,15 @@
    </xsl:choose>
 </xsl:template>
 
-<xsl:template match="APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con']" mode="pure">
+<xsl:template match="APPLY[instantiate/CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_sacs.con'] | APPLY[CONST/@uri='cic:/Coq/ring/Ring_abstract/interp_sacs.con']" mode="pure">
    <xsl:choose>
-      <xsl:when test="count(child::*) = 9 and *[APPLY and position()=9]
-                      [CONST/@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con']">
+      <xsl:when test="count(child::*) = 2 and *[APPLY and position()=2][CONST/@uri='cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con']">
          <m:apply helm:xref="{@id}">
             <m:csymbol>app</m:csymbol>
-            <xsl:apply-templates mode="noannot" select="*[9]/*[1]"/>
+            <xsl:apply-templates mode="noannot" select="*[2]/*[1]"/>
             <xsl:call-template name="start-interp">
-	       <xsl:with-param name="rtree" select="*[9]/*[2]"/>
-               <xsl:with-param name="atree" select="*[8]"/>
+	       <xsl:with-param name="rtree" select="*[2]/*[2]"/>
+            <xsl:with-param name="atree" select="instantiate/*[position() = last()]"/>
 	    </xsl:call-template>
          </m:apply>
       </xsl:when>
@@ -54,28 +53,34 @@
 
 <!-- **************************  abstract polinomials rendering ************************ -->
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
-                                    and @noConstr='1']]" mode="interp">
+<xsl:template match="*" mode="interp">
+ <m:apply>
+  <m:ci>ERROR INTERP:</m:ci>
+  <xsl:apply-templates select="." mode="noannot"/>
+ </m:apply>
+</xsl:template>
+
+<!-- APVar -->
+<!-- CSC: ??????????? -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='1']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:apply-templates select="*[2]" mode="interp">
       <xsl:with-param name="atree" select="$atree"/>
    </xsl:apply-templates>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
-                                    and @noConstr='2']]" mode="interp">
-   <xsl:param name="atree"/>
-   <xsl:apply-templates mode="noannot" select="."/>
+<!-- AP0 -->
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='2']" mode="interp">
+ <m:cn definitionURL="{@uri}" helm:xref="{@id}">0</m:cn>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
-                                    and @noConstr='3']]" mode="interp">
-   <xsl:param name="atree"/>
-   <xsl:apply-templates mode="noannot" select="."/>
+<!-- AP1 -->
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='3']" mode="interp">
+ <m:cn definitionURL="{@uri}" helm:xref="{@id}">1</m:cn>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
-                                    and @noConstr='4']]" mode="interp">
+<!-- APplus -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='4']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:call-template name="mk-mml-op-interp">
       <xsl:with-param name="arity" select="2"/>
@@ -85,8 +90,8 @@
    </xsl:call-template>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
-                                    and @noConstr='5']]" mode="interp">
+<!-- APmult -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='5']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:call-template name="mk-mml-op-interp">
       <xsl:with-param name="arity" select="2"/>
@@ -96,8 +101,8 @@
    </xsl:call-template>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind' 
-                                    and @noConstr='6']]" mode="interp">
+<!-- APopp -->
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Ring_abstract/apolynomial.ind' and @noConstr='6']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:call-template name="mk-mml-op-interp">
       <xsl:with-param name="arity" select="1"/>
@@ -107,24 +112,21 @@
    </xsl:call-template> 
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind' 
-                                    and @noConstr='1']]" mode="interp">
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' and @noConstr='1']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:apply-templates select="*[2]" mode="interp">
       <xsl:with-param name="atree" select="$atree/*[4]"/>
    </xsl:apply-templates>
 </xsl:template>
 
-<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind' 
-                                    and @noConstr='2']]" mode="interp">
+<xsl:template match="APPLY[MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' and @noConstr='2']]" mode="interp">
    <xsl:param name="atree"/>
    <xsl:apply-templates select="*[2]" mode="interp"> 
       <xsl:with-param name="atree" select="$atree/*[5]"/>
    </xsl:apply-templates>
 </xsl:template>
 
-<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/variables_map/index.ind' 
-                              and @noConstr='3']" mode="interp">
+<xsl:template match="MUTCONSTRUCT[@uri='cic:/Coq/ring/Quote/index.ind' and @noConstr='3']" mode="interp">
    <xsl:param name="atree"/>
    <xsl:apply-templates select="$atree/*[3]" mode="noannot"/>
 </xsl:template>
diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt
index 2f31b969a..84cd46836 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
@@ -12,9 +13,11 @@ html_init.xsl
 html_reals.xsl
 html_set.xsl
 inductive.xsl
+ite.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 +30,7 @@ objcontent.xsl
 objtheorycontent.xsl
 params.xsl
 proofs.xsl
+rewrite.xsl
 ricerca.xsl
 ring.xsl
 rootcontent.xsl
-- 
2.39.2