formal_map now defined

[helm.git] / helm / software / matita / library / datatypes / subsets.ma

diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma
index 5483dfa37f1fd648a38eca5727cd9cb9d05cc134..d6bcf4ddacf24944eb92fca355993a8266565c38 100644 (file)
--- a/helm/software/matita/library/datatypes/subsets.ma
+++ b/helm/software/matita/library/datatypes/subsets.ma
@@ -116,12 +116,15 @@ qed.
 
 interpretation "union" 'union U V = (fun1 ___ (union _) U V).
 
-definition singleton: ∀A:setoid. A → Ω \sup A.
- apply (λA:setoid.λa:A.{b | a=b});
- intros; simplify;
- split; intro;
- apply (.= H1);
-  [ apply H | apply (H \sup -1) ]
+definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
+ intros; constructor 1;
+  [ apply (λA:setoid.λa:A.{b | a=b});
+    intros; simplify;
+    split; intro;
+    apply (.= H1);
+     [ apply H | apply (H \sup -1) ]
+  | intros; split; intros 2; simplify in f ⊢ %; apply trans;
+     [ apply a |4: apply a'] try assumption; apply sym; assumption]
 qed.
 
-interpretation "singleton" 'singl a = (singleton _ a).
+interpretation "singleton" 'singl a = (fun_1 __ (singleton _) a).
\ No newline at end of file