change thin air rule

[ahuoguo]

Maybe should have the thin air rule as follows (from the completeness proof) and have another rule like ⊢ ↯(0)

Another consideration is in verisbelt it's hard to do typed_instr with the original encoding, and i only proved the err incr version
https://github.com/ahuoguo/verisbelt/pull/3/changes#diff-7328771b10fd40f66420783a1c5b9eeeeae5048221766b001dfcd000e1d4a0d8R119

[ahuoguo]

This is actually pretty hard to encode using verus pre/postcondition, since verus can't talk about wp impredicatively

I currently have

#[verus::trusted]
#[verifier::external_body]
pub fn thin_air() -> (ret: Tracked<ErrorCreditResource>)
    ensures
        // owns ↯(ε) for ε > 0
        exists |eps: real| eps > 0.0 && (ErrorCreditCarrier::Value { car: eps } =~= ret.view().view()),
{
    Tracked::assume_new()
}

which roughly looks like the original coneris version