Update snapshot predicate to exclude uninhabited discriminants

[zgrannan]

Fixes no-annotations/void.rs.

For functions likes

pub enum Void { }
fn void_unwrap<T>(this: Result<T, Void>) -> T {
    match this {
        Ok(val) => val,
        Err(e) => unreachable(e)
    }
}

Rust does not emit a discriminant check because there is only one inhabited case.

Prusti previously could not verify this example, because this constraint on the type was not encoded in Viper, and without knowing the discriminant, the permissions to val after the downcast could not be obtained.

This PR updates the encoding of types to assert that the variant index of an enum cannot equal the discriminant of an uninhabited variant.