Definition R16_NonEmpty := nil_cons (x := R16) (l := []).
