Extending a result due to Friedman and Sheard (1987), Cantini showed that VF is much stronger than KF: VF is proof-theoretically equivalent to the theory ID\(_1\) of non-iterated inductive definitions, which is not predicative. 