...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / relations_to_o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index c0cf12090b3808398b8ae814db479c92d0b77e59..9bcd51c7c0ece3c3acab8416844cf523e3f3df16 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -40,7 +40,7 @@ definition POW': objs1 SET → OAlgebra.
      [ assumption
      | whd; intros; cases i; simplify; assumption]
   | intros; split; intro;
-     [ cases f; cases x1; exists [apply w1] exists [apply w] assumption;
+     [ (** screenshot "screen-pow". *) cases f; cases x1; exists [apply w1] exists [apply w] assumption;
      | cases e; cases x; exists; [apply w1] [ assumption | exists; [apply w] assumption]]
   | intros; intros 2; cases (f {(a)} ?); 
      [ exists; [apply a] [assumption | change with (a = a); apply refl1;]