exhaustivity completed

[helm.git] / helm / software / matita / contribs / dama / dama / uniform.ma

diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma
index d5d71472688632790a6545620ab6caca33398fb5..41b593ae4a25832cc073a98c0702235f1c39be84 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/uniform.ma
@@ -139,5 +139,3 @@ interpretation "explicit big set" 'explicitset t =
 definition restrict_uniformity ≝
   λC:uniform_space.λX:C→Prop.
    {U:C square → Prop| (U ⊆ {x:C square|X (fst x) ∧ X(snd x)}) ∧ us_unifbase C U}.
-
-