take k const 0 ; :: thesis: k const 0 is k -ary
thus k const 0 is k -ary ; :: thesis: verum