proposition: Lemma subterm_fun_elim : forall u f ts, subterm u (Fun f ts) -> exists t, In t ts /\ subterm_eq u t.
proof: Proof. intros. destruct H as [C [CH fC]]. destruct C. intuition. simpl in fC. injection fC. intros. subst ts. exists (fill C u). split. auto with datatypes. unfold subterm_eq. exists C. refl. Qed.
imports: CoLoR(LogicUtil) CoLoR(ListUtil)