rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
elim H1.
- applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
+ pump 39.
+ applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
(*
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.