Definition R64_NonEmpty := nil_cons (x := R64) (l := []).
