proposition: Theorem in_multpf_head : forall (p q : list (Term A n)) (a b : Term A n), canonical A0 eqA ltM (pX a p) -> canonical A0 eqA ltM (pX b q) -> In (multTerm (A:=A) multA (n:=n) a b) (multpf (pX a p) (pX b q)).
proof: Proof. Proof using os. intros p q a b H' H'0. elim (multpf_head p q a b); [ intros c E; rewrite E | idtac | idtac ]; simpl in |- *; auto. Qed.