take seq_const 0 ; :: thesis: seq_const 0 is constant
thus seq_const 0 is constant ; :: thesis: verum