proposition: Lemma subterm_fun : forall f ts u, Vin u ts -> subterm u (Fun f ts).
proof: Proof. intros. unfold subterm. assert (exists n1, exists v1 : terms n1, exists n2, exists v2 : terms n2, exists H : n1 + S n2 = arity f, ts = Vcast (Vapp v1 (Vcons u v2)) H). apply Vin_elim. hyp. destruct H0 as [n1]. destruct H0 as [ts1]. destruct H0 as [n2]. destruct H0 as [ts2]. destruct H0 as [H1]. exists (Cont H1 ts1 Hole ts2). split. discr. rewrite H0. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)