proposition: Theorem spolyf_canonical : forall (p q : list (Term A n)) (Cp : canonical A0 eqA ltM p) (Cq : canonical A0 eqA ltM q), canonical A0 eqA ltM (spolyf p q Cp Cq).
proof: Proof. Proof using plusA os cs. intros p; case p; simpl in |- *; auto. intros a l q; case q; unfold LetP in |- *; simpl in |- *; auto. intros a0 l0 H' H'0. cut (canonical A0 eqA ltM l0); [ intros Op1 | apply canonical_imp_canonical with (a := a0) ]; auto. cut (canonical A0 eqA ltM l); [ intros Op2 | apply canonical_imp_canonical with (a := a) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ intros Z0 | apply canonical_nzeroP with (ltM := ltM) (p := l); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) a0); [ intros Z1 | apply canonical_nzeroP with (ltM := ltM) (p := l0) ]; auto. Qed.