non-termination

Im dritten Kapitel der CPDT wird kurz erläutert, warum negative induktive Typen in Coq verboten sind. Wenn wir hätten %Vor% Dann könnten wir einfach eine Funktion definieren %Vor% , so dass der Ausdruck uhoh (Abs uhoh) nicht terminiere...