X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations_to_o-algebra.ma;h=842219280ba10fcfe19eba1af70f08b4f8944197;hb=e607b42a9a469b02ef377210dc34ada14cc603c1;hp=bc13ecfd7ee5ee6e259630e5a1a18a8c0de76a26;hpb=ddc0a7b3f0acd57f879e540e696f69ca0c20bbf5;p=helm.git

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 bc13ecfd7..842219280 100644
--- 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
@@ -200,7 +200,7 @@ qed.
 *)
 
 interpretation "lifting singl" 'singl x = 
- (fun11 _ (objs2 (POW _))  (singleton _) x).
+ (fun11 ? (objs2 (POW ?))  (singleton ?) x).
 
 theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f).
  intros; exists;