`mrec-fix` is currently defined with a `let` (issue #170, PR #171), which, sadly, gets simplified away with `cbn`/`simpl`. One solution may be to make the `D : Type -> Type` argument explicit.
mrec-fixis currently defined with alet(issue #170, PR #171), which, sadly, gets simplified away withcbn/simpl.One solution may be to make the
D : Type -> Typeargument explicit.