Well-founded induction

Well-founded induction is a generalisation of mathematical induction. While simple induction allows for 𝑃𝑥 to be proven by assuming 𝑃 holds for the "structural predecessors"Some examples: the structural predecessor of a natural number 𝑆𝑛 is 𝑛; of a cons cell of a linked list, the predecessor is the tail; of a binary tree node, the predecessors are the two immediate children. of 𝑥, the more powerful well-founded induction allows you to prove 𝑃𝑥 assuming 𝑃(𝑦) holds for all 𝑦 < 𝑥, where < is some well-founded relation.