From 6454e0578b1b3b3bb7c9f9a60946e1a4c2f97ff3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 Dec 2008 18:12:47 +0000
Subject: [PATCH] Some fixes.

---
 .../contribs/formal_topology/overlap/o-concrete_spaces.ma    | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
index 5b08b5917..9cbaada80 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -47,7 +47,8 @@ lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed
 coercion xxx nocomposites.
 
 lemma down_p : ∀S,I:SET.∀u:S⇒S.∀c:arrows1 SET I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a').
-intros; unfold uncurry_arrows; apply (†(†H));
+intros; unfold uncurry_arrows; change in c with (I ⇒ S);
+apply (†(†H));
 qed.
 
 alias symbol "eq" = "setoid eq".
@@ -122,7 +123,7 @@ definition convergent_relation_space_composition:
  ∀o1,o2,o3: concrete_space.
   binary_morphism1
    (convergent_relation_space_setoid o1 o2)
-   (convergentin ⊢ (? (? ? ? (? ? ? (? ? ? ? ? (? ? ? (? ? ? (% ? ?))) ?)) ?) ? ? ?)_relation_space_setoid o2 o3)
+   (convergent_relation_space_setoid o2 o3)
    (convergent_relation_space_setoid o1 o3).
  intros; constructor 1;
      [ intros; whd in c c1 ⊢ %;
-- 
2.39.2