From 473f04c051fae559d1598e8e1a3f3bf5e43cbe64 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Feb 2008 11:00:54 +0000 Subject: [PATCH] snapshot --- helm/software/matita/dama/lattice.ma | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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; -- 2.39.2