Abstract
A formalized coinductive account of the abstract development of
Brotherston, Gorogiannis, and Petersen [APLAS 2012], in a slightly
more general form since we work with arbitrary infinite proofs, which
may be acyclic. This work is described in detail in an article by the
authors, published in 2017 in the Journal of Automated
Reasoning. The abstract proof can be instantiated for
various formalisms, including first-order logic with inductive
predicates.