nasty change in the lexer/parser:

[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 af3015eb368737d5f62f3ce5c8689399edfc9e07..842219280ba10fcfe19eba1af70f08b4f8944197 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
@@ -182,8 +182,25 @@ theorem POW_faithful:
   |*: cases Hletin; cases x1; change in f3 with (x =_1 w); apply (. f3‡#); assumption;]
 qed.
 
+
+lemma currify: ∀A,B,C. binary_morphism1 A B C → A → unary_morphism1 B C.
+intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
+qed.
+
+(*
+alias symbol "singl" = "singleton".
+alias symbol "eq" = "setoid eq".
+lemma in_singleton_to_eq : ∀A:setoid.∀y,x:A.y ∈ {(x)} → (eq1 A) y x.
+intros; apply sym1; apply f;
+qed.  
+
+lemma eq_to_in_singleton : ∀A:setoid.∀y,x:A.eq1 A y x → y ∈ {(x)}.
+intros; apply (e^-1);
+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;