James Brotherston and Alex Simpson worked on *non*-well-founded proofs, see > J. Brotherston and A. Simpson: [Sequent calculi for induction and infinite descent][1]. J Logic Computation (2010) as well as the talk "[On Proof by Innite Descent][2]" by Alex Simpson at "Algebra & Coalgebra meet Proof Theory" in Bern, April 2012. [1]: http://logcom.oxfordjournals.org/content/early/2010/09/30/logcom.exq052.abstract [2]: http://homepages.inf.ed.ac.uk/als/Talks/infinite_descent.pdf