Description: ax-ext with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010)