Great: some significant progress in fixing universe levels.

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / subsets.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 73872bfed5f8bceeb5605d28fd614abb6fe83cc9..6351fead91eca85d504ca36b96a93d70a4153db2 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -203,7 +203,7 @@ definition SUBSETS: objs1 SET → OAlgebra.
        (* senza questa change, universe inconsistency *)
        change in ⊢ (? ? (λ_:%.?)) with (carr I);
        exists [apply w1] exists [apply w] assumption;
-     | cases H; cases x; exists; [apply w1]
+     | cases e; cases x; exists; [apply w1]
         [ assumption
         | (* senza questa change, universe inconsistency *)
           whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);