fact: Fixpoint processInt (ri : rawTrsInt) : option (list symInt) := match ri with | nil => Some nil | cons i is => match checkInt (fst i) (snd i) with | None => None | Some fi => match processInt is with | None => None | Some fis => Some (fi :: fis) end end end.
imports: Coq(Program) CoLoR(LogicUtil OptUtil ATrs NaryFunction AInterpretation Proof ListUtil)