Def (rec) (basepower) == if power=0 1 else base(basepower-1) fi

Thm* n,k:. (nk)

Thm* n,k:. (nk)

Def i=j == if i=jtrue; false fi

Thm* i,j:. i=j