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