fact: Parameter size_subterm_at_pos : forall t i p, match subterm_at_pos t (i :: p) with | Some u => size u < size t | None => True end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)