…completeness

fix #885, and non-deterministic incompleteness for cases like:

```rust
trait T {
    spec fn a() -> bool;
    proof fn p() ensures Self::a();
    proof fn q() ensures Self::a();
}

struct S { pub dummy: nat }
impl T for S {
    spec fn a() -> bool;
    proof fn p() { Self::q(); }
    proof fn q() { /* ... */  }
}
```

without this change, Self::p was sometimes lowered to AIR without having processed
Self::q first, which was not found as a function with a postcondition,
which resulted in the encoding for `p()` to be an empty block instead of
the expected `(assume <q's postcondition>)`.

… SCC ordering

fix #885, and non-deterministic incompleteness for cases like:

```rust
trait T {
    spec fn a() -> bool;
    proof fn p() ensures Self::a();
    proof fn q() ensures Self::a();
}

struct S { pub dummy: nat }
impl T for S {
    spec fn a() -> bool;
    proof fn p() { Self::q(); }
    proof fn q() { /* ... */  }
}
```

without this change, Self::p was sometimes lowered to AIR without having processed
Self::q first, which was not found as a function with a postcondition,
which resulted in the encoding for `p()` to be an empty block instead of
the expected `(assume <q's postcondition>)`.

… SCC ordering

fix #885, and non-deterministic incompleteness for cases like:

```rust
trait T {
    spec fn a() -> bool;
    proof fn p() ensures Self::a();
    proof fn q() ensures Self::a();
}

struct S { pub dummy: nat }
impl T for S {
    spec fn a() -> bool;
    proof fn p() { Self::q(); }
    proof fn q() { /* ... */  }
}
```

without this change, Self::p was sometimes lowered to AIR without having processed
Self::q first, which was not found as a function with a postcondition,
which resulted in the encoding for `p()` to be an empty block instead of
the expected `(assume <q's postcondition>)`.