λA,B.λf: pre_magma_morphism A B. match f with [ mk_pre_magma_morphism f _ ⇒ f ].
ncoercion mmcarr: ∀A,B.∀M: pre_magma_morphism A B. A → B ≝ mmcarr
on _M: pre_magma_morphism ? ? to ∀_.?.
+ndefinition mmprop ≝
+ λA,B,M.
+ match M return λM:pre_magma_morphism A B.∀x,y. M (op ? x y) = op ? (M x) (M y) with
+ [ mk_pre_magma_morphism _ p ⇒ p ].
nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type ≝
{ mmmcarr: pre_magma_morphism A B;
[ napply (op ? x0 y0)
| napply (conj ????)
[ napply (op_closed ??????); nassumption
- | nelim daemon ]##]
+ | (* nrewrite < Hx1; DOES NOT WORK *)
+ napply (eq_rect ?? (λ_.?) ?? Hx1);
+ napply (eq_rect ?? (λ_.?) ?? Hy1);
+ napply (mmprop ?? f ??)]##]
nqed.
\ No newline at end of file