take seq_const 0 ; :: thesis: seq_const 0 is RAT -valued
thus seq_const 0 is RAT -valued ; :: thesis: verum