From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 4 Feb 2008 11:00:54 +0000 (+0000)
Subject: snapshot
X-Git-Tag: make_still_working~5636
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=473f04c051fae559d1598e8e1a3f3bf5e43cbe64;p=helm.git

snapshot
---

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 88db12061..0b464aeec 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -333,7 +333,10 @@ lemma subst_excess_base_in_semi_lattice:
 intros (sl eb H H1 H2 H3 H4); 
 apply (subst_excess sl);
   [apply (subst_excess_base_in_excess sl eb H H1 H2);
-  |rewrite > (subst_excess_preserves_aprtness sl);
+  |apply subst_excess_base_in_excess_preserves_apartness;
+  |
+  unfold apartness_OF_semi_lattice;
+   letin xxx \def subst_excess_preserves_aprtness; clearbody xxx;
   
   
   clear H3 H4; unfold apartness_OF_semi_lattice;