Formally self-referential propositions for cut free classical analysis and related systems - Kreisel G; Takeuti G (Warezawa Panstwowe Wydawnictwo Naukowe, 1970)
Appendix 44-48p