proposition: Theorem CombLinear_incl : forall (a : list (Term A n)) (P Q : list (poly A0 eqA ltM)), (forall a : list (Term A n), inPolySet A A0 eqA n ltM a P -> inPolySet A A0 eqA n ltM a Q) -> CombLinear P a -> CombLinear Q a.
proof: Proof. Proof using os minusA invA divA cs A1. intros a P Q H' H'0; elim H'0; auto. intros a0 p q s H'1 H'2 H'3 H'4 H'5. apply CombLinear_comp with (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a0 q) p); auto. apply eqp_imp_canonical with (1 := cs) (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a0 q) p); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply canonical_pluspf with (1 := os); auto. apply canonical_mults with (1 := cs); auto. apply inPolySet_imp_canonical with (L := P); auto. apply CombLinear_canonical with (Q := Q); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.