X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Flattice.ma;h=768c86df1c2af47785bf08b8a762524e72be9426;hb=c38c15fa800498bcac6230e07a31ed54414a0865;hp=d6b637a0d35990479747b897ed5300b9e09dd0db;hpb=39c55604f8114e2e8f9f9769acd328de8f19c7e4;p=helm.git

diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/dama/lattice.ma
index d6b637a0d..768c86df1 100644
--- a/helm/software/matita/dama/lattice.ma
+++ b/helm/software/matita/dama/lattice.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/lattice/".
 
-include "excedence.ma".
+include "excess.ma".
 
 record lattice : Type ≝ {
   l_carr:> apartness;
@@ -40,8 +40,8 @@ interpretation "Lattice join" 'or a b =
 
 definition excl ≝ λl:lattice.λa,b:l.a # (a ∧ b).
 
-lemma excedence_of_lattice: lattice → excedence.
-intro l; apply (mk_excedence l (excl l));
+lemma excess_of_lattice: lattice → excess.
+intro l; apply (mk_excess l (excl l));
 [ intro x; unfold; intro H; unfold in H; apply (ap_coreflexive l x);
   apply (ap_rewr ??? (x∧x) (meet_refl l x)); assumption;
 | intros 3 (x y z); unfold excl; intro H;
@@ -55,7 +55,7 @@ intro l; apply (mk_excedence l (excl l));
   assumption]
 qed.    
 
-coercion cic:/matita/lattice/excedence_of_lattice.con.
+coercion cic:/matita/lattice/excess_of_lattice.con.
 
 lemma feq_ml: ∀ml:lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
 intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
@@ -69,7 +69,7 @@ qed.
 
 lemma le_to_eqm: ∀ml:lattice.∀a,b:ml. a ≤ b → a ≈ (a ∧ b).
 intros (l a b H); 
-  unfold le in H; unfold excedence_of_lattice in H;
+  unfold le in H; unfold excess_of_lattice in H;
   unfold excl in H; simplify in H; 
 unfold eq; assumption;
 qed.