excede->excess

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

diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 827aaf605c621a6df1ccb30f82a409827cdce865..061d2db9be34c33904e89ffad0b9cdfa634af351 100644 (file)
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -132,7 +132,7 @@ lapply (exc_coreflexive E) as r; unfold coreflexive in r;
 |2: lapply (c ?? x H2) as H3; cases H3 (H4 H4); [right; assumption|cases (Lxy H4)]]
 qed.
 
-theorem lt_to_excede: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a).
+theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a).
 intros (E a b Lab); cases Lab (LEab Aab);
 cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)  
 qed.