+ | napply (conj ????)
+ [ napply (op_closed ??????); nassumption
+ | nrewrite < Hx1;
+ nrewrite < Hy1;
+ napply (mmprop ?? f ??)]##]
+nqed.
+
+ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
+ λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
+
+ndefinition mm_counter_image:
+ ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma A.
+ #A; #B; #Ma; #Mb; #f;
+ napply (mk_magma ???)
+ [ napply (counter_image ?? f Mb)
+ | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
+ napply (ex_intro ????)
+ [ napply (op ? x0 y0)
+ | napply (conj ????)
+ [ napply (op_closed ??????); nassumption
+ | nrewrite < Hx1;
+ nrewrite < Hy1;
+ napply (mmprop ?? f ??)]##]