In this talk, I present a framework for recursive proofs of coinductive predicates, which are defined via functor liftings to fibrations. This framework is based on the so-called later modality and Löb-induction. Intuitively, the role of the later modality is thereby to control the use of coinduction hypotheses. Since the framework works on certain fibrations, it can be instantiated in very diverse situation like, for instance, set-based predicates and relations, quantitative predicates and relations, syntactic first-order logic, or dependent type theory. Apart from showing the underlying technical constructions of the framework, I will demonstrate how it can be used in those examples. Moreover, I will briefly talk about some recent progress, in collaboration with Katya Komendantskaya and Yue Li, in the direction of automatic proof search for this framework.