Twierdzenie o niepustym barze, czyli zmechanizowana naturalna dedukcja Jacek Chrząszcz informatyka Delta 4/2017