proposition: Lemma subterm_fun_elim : forall u f ts, subterm u (Fun f ts) -> exists t, Vin t ts /\ subterm_eq u t.
proof: Proof. intros. unfold subterm in H. destruct H as [C]. destruct H. destruct C. cong. clear H. simpl in H0. Funeqtac. subst ts. exists (fill C u). split. apply Vin_cast_intro. apply Vin_app_cons. unfold subterm_eq. exists C. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)