Inlining of Dedekind cuts not always sound

[bmsherman]

marshall/src/eval.ml

Lines 188 to 196 in 65f20eb

	match e1' with
	| S.Cut (x, i, p1, p2) ->
	hnf env (S.App (S.Lambda (x, S.Ty_Real, p2), e2))
	| _ ->
	list_bind (hnf env e2) (fun e2' ->
	match e2' with
	| S.Cut (x, i, p1, p2) ->
	hnf env (S.App (S.Lambda (x, S.Ty_Real, p1), e1'))
	| _ -> [S.Less (e1', e2')]

This is valid if the interval of the Dedekind cut is [-inf, inf], but if the interval is smaller, that needs to be incorporated in the inlining.

See how, e.g., sqrt pi is broken because of this.