proposition: Theorem spolyf_pO : forall (a : list (Term A n)) (Ca : canonical A0 eqA ltM a), eqP A eqA n (spolyf a a Ca Ca) (pO A n).
proof: Proof. Proof using plusA os cs. intros a; case a; simpl in |- *; unfold LetP in |- *; auto. intros; apply minuspf_refl with (1 := cs); auto. Qed.