(* qua non riesco a mettere set *)
definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
intros; constructor 1;
- [ apply (λa:A.{b | eq ? a b}); unfold setoid1_of_setoid; simplify;
+ [ apply (λa:A.{b | a =_0 b}); unfold setoid1_of_setoid; simplify;
intros; simplify;
split; intro;
apply (.= e1);