all pullbacks are attempted in sequence, removed many unfold

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index b17dacbaf8a01ab107d8cd24914f9599899e511b..b278adfc0541b82b714eb1df4dce3e2f7496c41c 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -286,8 +286,7 @@ constructor 1;
     apply or_prop3;
   ]
 | intros; split; simplify; 
-   [3: unfold arrows1_of_ORelation_setoid;
-         apply ((†e)‡(†e1));
+   [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
    |1: apply ((†e)‡(†e1));
    |2,4: apply ((†e1)‡(†e));]]
 qed.