Test for #3542 fixed some time ago.
Fixing #3562 ("as" in "destruct" expects either a disjunctive
intropattern or a bound ltac variable).