Definition R8_NonEmpty := nil_cons (x := R8) (l := []).
