take 0_. R ; :: thesis: 0_. R is zero
thus 0_. R is zero ; :: thesis: verum