Tengo un conjunto inductivo construido con tres constructores:

Inductive MF : Set :=
| D : MF
| cn : MF -> MF -> MF
| dn : Z -> MF -> MF.

Me gustaría definir de alguna manera un nuevo conjunto inductivo B, de modo que B sea un subconjunto de MF que contenga solo los elementos obtenidos de D y dn. Además, todo en B debe interpretarse como tipo MF si es necesario.

Intenté definir primero B y luego MF de la siguiente manera:

Inductive B : Set :=
| D : B
| dn : Z -> B -> B.

Inductive MF : Set :=
| m : B -> MF
| cn : MF -> MF -> MF
| Dn : Z -> MF -> MF.
Axiom m_inj : forall (a b : B), m a = m b -> a = b.
Coercion m : B >-> MF.
Axiom dnDn : forall (a : B)(i : Z), (m (dn i a)) = (Dn i (m a)).

El problema aquí es que tengo constructores (dn y Dn) que deben ser intercambiables con respecto a los elementos en B. Esto me da muchos problemas en desarrollos posteriores y tengo que seguir agregando Axiomas para obtener el comportamiento deseado.