 The saturation condition 10. still has to be added independent of which option is considered. The principle was applied in Benzmüller 1999a,b to prove completeness for the extensional higher-order  RUE-resolution[3]  calculus underlying the higher-order automated theorem prover LEO and its successor LEO-II.