proposition: Theorem reducehead_imp_reduce : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), reducehead Q p q -> reduce Q p q.
proof: Proof. Proof using plusA cs. intros Q p q H'; elim H'; auto. intros a b nZb p0 q0 H'0. apply reducetop with (b := b) (nZb := nZb) (q := q0); auto. apply pick_inv_in with (a := a); auto. apply pick_inv_eqT with (Q := Q) (q := q0); auto. Qed.