fact: Parameter var_in_subterm2 : forall v t, mem (@eq _) v (var_list t) -> {p : list nat | subterm_at_pos t p = Some (Var v)}.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)