Definition R32_NonEmpty := nil_cons (x := R32) (l := []).
