take ArProg (0,0) ; :: thesis: ArProg (0,0) is constant
thus ArProg (0,0) is constant ; :: thesis: verum