fact: Fixpoint subterm_pos (t : term) (ps : position) {struct ps} : option term := match t, ps with | _ , nil => Some t | Var x , _ :: _ => None | Fun f ts, p :: ps' => match lt_ge_dec p (arity f) with | left h => subterm_pos (Vnth ts h) ps' | right _ => None end end.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)