Description: Alternate version of ac6 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008) (Revised by Thierry Arnoux, 17-May-2020)