fact: Fixpoint subterm_at_pos (t : term) (p : list nat) {struct p}: option term := match p with | nil => Some t | i :: q => match t with | Var _ => None | Term _ l => match nth_error l i with | Some ti => subterm_at_pos ti q | None => None end end end.
imports: List more_list list_permut list_set Arith