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