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