Well-Founded Relation

A Relation R : A A Ω : 𝑅 𝐴 𝐴 Ω R:A\to A\to\Omega is well-founded if we can do induction down it; EG:

((x:A).((y:A).R(y,x)P(y))P(x))(x:A).P(x)\par(\forall(x:A).\;(\forall(y:A).\;R(y,x)\to P(y))\to P(x))\to\forall(x:A).\;% P(x)

For every P : A 𝖴 : 𝑃 𝐴 𝖴 P:A\to\mathsf{U}{} .