Soundness of all(..)

[bvssvni]

Currently, this just lifts the entire expression without any checks on soundness.

Needs to be investigated in detail.

[bvssvni]

It is unsound when you can prove all(a -> b):

fn test_all all(a -> b) {
    x : all(a);
    return x;
}

fn test_absurd true -> a {
    use test_all;

    x : true;
    let y = test_all(x) : a;
    return y;
}