proposition: Lemma tdivGoodP : forall (F : list trm) (f : trm), Bad F -> (forall g : trm, In g F -> ~ tdiv g f) -> Bad (f :: F).
proof: Proof. intros F f H' H'0; red in |- *. intros H'1; inversion H'1; auto. apply tdivExists_trmHd_lem with (F := F) (f := f); auto. Qed.
imports: Coq(List)