Second order permutative conversions with Prawitz's strong validity
Makoto Tatsuta · Progress in Informatics · 2005
A clear and complete proof of strong normalization of second order natural deduction with permutative conversions is given by using Prawitz's strong validity.This paper completes Prawitz's original proof.