simplified some proofs thanks to auto sledgehammer