proposition: Theorem eqp_invT1_pO_is_pO : forall p : list (Term A n), eqP A eqA n (mults (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p) (pO A n) -> eqP A eqA n p (pO A n).
proof: Proof. intros p; case p; simpl in |- *; auto. intros a l H'; inversion H'. Qed.