X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fsubsets.ma;h=6351fead91eca85d504ca36b96a93d70a4153db2;hb=c78cbede35ed85575e274864e6b6b9c635c6956d;hp=73872bfed5f8bceeb5605d28fd614abb6fe83cc9;hpb=279b11c00cdaacb4858e1c8dc6d05ea631bc1358;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 73872bfed..6351fead9 100644
--- 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);