Thankfully, we can't use them, because they would create circular proofs, but they are still given as options