fact: Parameter var_in_subterm : forall v s t p, subterm_at_pos t p = Some s -> In v (var_list s) -> In v (var_list t).
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)