From cb89a1eebdd620d7e1c593fa279e74d4c715b8bf Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 26 Nov 2007 10:52:53 +0000
Subject: [PATCH] pretty

---
 helm/software/matita/dama/valued_lattice.ma | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/helm/software/matita/dama/valued_lattice.ma b/helm/software/matita/dama/valued_lattice.ma
index 6ad88424a..165160977 100644
--- a/helm/software/matita/dama/valued_lattice.ma
+++ b/helm/software/matita/dama/valued_lattice.ma
@@ -90,7 +90,7 @@ qed.
 lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))).
 intros (R L x y z);
 lapply (modular_mjp ?? x (y ∨ z)) as H1;
-apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z)))); [2: apply feq_plusr; apply H1;] clear H1;
+apply (eq_trans ?? (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ?? (feq_plusr ???? H1)); clear H1;
 apply (eq_trans ?? ? ?? (plus_comm ???));
 apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????));
 apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??));
@@ -103,8 +103,8 @@ intros (R L x y z);
 lapply (modular_mjp ?? x (y ∧ z)) as H1;
 apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
 apply (eq_trans ?? ? ?? (plus_comm ???));
-apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z))); [2: apply eq_sym; apply plus_assoc]
-apply (eq_trans ?? (0+ μ(x∨y∧z))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse]
+apply (eq_trans ?? (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ?? (plus_assoc ????));
+apply (eq_trans ?? (0+ μ(x∨y∧z)) ?? (opp_inverse ??));
 apply eq_sym; apply zero_neutral;
 qed.
 
-- 
2.39.2