ABSTRACT. We present Tores, a language for logical reasoning which utilizes indexed types and flexible (co)recursion principles to allow encoding of metatheoretic proofs. We particularly target the encoding of proofs using the technique of logical relations. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types together with a form of recursion over objects in the index language to build new types. The latter, which we call index-stratified types, are analogue to the concept of large elimination in dependently typed languages. These features combined allow us to encode sophisticated case studies such as normalization for lambda calculi and normalization by evaluation. We prove the soundness of Tores as a programming and proof language via the key theorems of subject reduction and termination.