Resources can be used on left of implication in assumes

[totoyoyo]

Impure expressions are typically not allowed on the LHS of an implication, except in an assume :

field val: Int

method foo(r: Ref) 
    requires acc(r.val) ==> true
    ensures acc(r.val) ==> true
{
    assume acc(r.val) ==> true
    assert acc(r.val) ==> true 

    inhale acc(r.val) ==> true
    exhale acc(r.val) ==> true
}

In the above example, all uses of acc(r.val) are not allowed except for assume acc(r.val) ==> true. Isn't this a bit inconsistent, especially if you cannot assert something you have assumed?