proposition: Lemma tdivExists_trmHd_lem : forall (F : list trm) (f : trm), (forall g : trm, In g F -> ~ tdiv g f) -> ExistsL trm (fun g : trm => tdiv g f) F -> False.
proof: Proof. intros F; elim F; simpl in |- *; auto. intros f H' H'0; inversion H'0; auto. intros a l H' f H'0 H'1; inversion H'1; auto. lapply (H'0 a); [ intro H'3; apply H'3 | idtac ]; auto. apply H' with (f := f); auto. Qed.
imports: Coq(List)