snapshot

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 88db1206128f2f2c3cd6b40369689739b2d53e32..0b464aeec87017c084a40f3403f3a18ddc09a840 100644 (file)
--- 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;