cleanup of the eq_trans burdain

[helm.git] / helm / software / matita / dama / lattice.ma

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index 9e91376d17bbe2be3dd82b0bd58b45454b032f04..d6b637a0d35990479747b897ed5300b9e09dd0db 100644 (file)
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -77,9 +77,9 @@ qed.
 lemma le_to_eqj: ∀ml:lattice.∀a,b:ml. a ≤ b → b ≈ (a ∨ b).
 intros (l a b H); lapply (le_to_eqm ??? H) as H1;
 lapply (feq_jl ??? b H1) as H2;
-apply (eq_trans ????? (join_comm ???));
-apply (eq_trans ?? (b∨a∧b) ?? H2); clear H1 H2 H;
-apply (eq_trans ?? (b∨(b∧a)) ?? (feq_jl ???? (meet_comm ???)));
+apply (Eq≈ ?? (join_comm ???));
+apply (Eq≈ (b∨a∧b) ? H2); clear H1 H2 H;
+apply (Eq≈ (b∨(b∧a)) ? (feq_jl ???? (meet_comm ???)));
 apply eq_sym; apply absorbjm;
 qed.