reconsider G = {{}} as SimpleGraph ;
take G ; :: thesis: G is void
thus G is void ; :: thesis: verum