nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type[0] ≝
{ mmmcarr:> magma_morphism_type A B;
nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type[0] ≝
{ mmmcarr:> magma_morphism_type A B;
| #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
napply conj; napply op_closed; nassumption ]
nqed.
\ No newline at end of file
| #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
napply conj; napply op_closed; nassumption ]
nqed.
\ No newline at end of file