Ich habe ein Induktives Set mit drei Konstruktoren gebaut:

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

Ich möchte irgendwie eine neue induktive Menge B definieren, so dass B eine Teilmenge von MF ist, die nur die aus D und dn erhaltenen Elemente enthält. Außerdem sollte bei Bedarf alles in B als Typ MF interpretiert werden.

Ich habe versucht, zuerst B und dann MF wie folgt zu definieren:

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)).

Das Problem hierbei ist, dass ich Konstruktoren (dn und Dn) haben muss, die in Bezug auf die Elemente in B austauschbar sein sollten. Dies bereitet mir eine Menge Probleme bei der Weiterentwicklung und ich muss immer wieder Axiome hinzufügen, um das beabsichtigte Verhalten zu erzielen .