Лекция 2. С.Л.Кузнецов. Теорема об устранении сечения для интуиционистского исчисления высказываний.