Certified Infinite Descent Criteria by Jamie Wright, Liron Cohen, Reuben Rowe and Andrei Popescu Jun 11