thus 1 = succ 0
.= {0 } ; :: thesis: verum