Well-Founded Relation

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

$\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\to\mathsf{U}{}