Fix-Point Equations for Well-Founded Recursion in Type Theory. - Antonia Balaa; Yves Bertot (TPHOLs, 2000)