proposition: Lemma subterm_eq_vars : forall u t x, subterm_eq u t -> List.In x (vars u) -> List.In x (vars t).
proof: Proof. unfold subterm_eq. intros. destruct H as [C]. subst t. elim C; clear C. simpl. hyp. intros. simpl fill. rewrite vars_fun, vars_vec_cast, vars_vec_app, vars_vec_cons. apply in_appr. apply in_appl. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)