take ConwayZero ; :: thesis: ConwayZero is zero
thus ConwayZero is zero ; :: thesis: verum