Some notes on: ``A deduction theorem for restricted generality''.
Martin W. Bunder · Notre Dame Journal of Formal Logic · 1976
In Axiom 2. \-Lx^x Exx. Axiom 3. \-Lx ~3x>y : xu D. yuv ^> xu. Axiom 4. \-Lx^> x ,t : xu ^>u yu(tu) ^>y . (xu => (yuv ^>v zuv)) ^>x (xu ^uzu(tu)). Axiom 5. hLx ^>x x (WQ). Axiom 6. HIH. Axiom 7. h-LH.