-
-ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
- λA,B,f,Sa. {y | ∃x. x ∈ Sa ∧ f x = y}.
+(*
+(* qui non funziona una cippa *)
+ndefinition image: ∀A,B. (carr A → carr B) → Ω \sup A → Ω \sup B ≝
+ λA,B:setoid.λf:carr A → carr B.λSa:Ω \sup A.
+ {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq B) ? ?(*(f x) y*)}.
+ ##[##2: napply (f x); ##|##3: napply y]
+ #a; #a'; #H; nwhd; nnormalize; (* per togliere setoid1_of_setoid *) napply (mk_iff ????);
+ *; #x; #Hx; napply (ex_intro … x)
+ [ napply (. (#‡(#‡#)));