Negative coverage: `borrow_check_statement` / `let` / premise `prove_ty_is_wf(env, assumptions, state, ty) => state`

Premise at line 188. Observed failure causes: failed_judgment.

let

Line	Coverage	Source
188	1	(prove_ty_is_wf(env, assumptions, state, ty) => state)
191	✗	(for_all(init in init.into_iter()) with (state) // FIXME: should make syntax for this (let Init { expr } = init) (borrow_check_expr_has_ty(env, assumptions, state, expr, ty, LiveBefore::live_before(&Assignment(id), env, &state, &places_live_on_exit), ) => state))
201	✗	(let state = state.with_local_in_scope(&env.env, label, id, ty)?)
202	N/A	(let state = if init.is_none() { state.with_uninit(&PlaceExpr::Var(id.clone())) } else { state.with_initialized(&PlaceExpr::Var(id.clone())) })
		──────── ("let")
204	55	(borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init }, places_live_on_exit) => (env, state))

1 test failed proving this premise:

Source location: tests/mir_typeck.rs:266

fn foo() -> () {
    let s2: S2<S1>;
}

Failed proof tree

check_all_crates failed mod.rs:41
- rule "check all prefixes" mod.rs:53
  - check_crate failed mod.rs:60
    
    rule "check crate" mod.rs:73
    
    check_crate_item failed mod.rs:163
    
    rule "free fn" mod.rs:191
    
    check_free_fn failed fns.rs:14
    
    rule "check free fn" fns.rs:24
    
    check_fn failed fns.rs:31
    
    rule "check fn" fns.rs:55
    
    check_fn_body failed fns.rs:62
    
    rule "expr fn body" fns.rs:90
    
    borrow_check failed nll.rs:126
    
    rule "borrow_check" nll.rs:137
    
    borrow_check_block failed nll.rs:144
    
    rule "basic block" nll.rs:159
    
    borrow_check_statement failed nll.rs:176
    
    rule "let" nll.rs:188
    
    prove failed function.rs:250
    
    rule function.rs:250
    
    prove_wc_list failed prove_wc_list.rs:11
    
    rule "some" prove_wc_list.rs:29
    
    prove_wc failed prove_wc.rs:23
    
    rule "parameter well formed" prove_wc.rs:161
    
    prove_wf failed prove_wf.rs:14
    
    rule "ADT" prove_wf.rs:67
    
    prove_after failed prove_after.rs:8
    
    rule "prove_after" prove_after.rs:19
    
    prove failed prove_after.rs:19
    
    rule prove_after.rs:19
    
    prove_wc_list failed prove_wc_list.rs:11
    
    rule "some" prove_wc_list.rs:29
    
    prove_wc failed prove_wc.rs:23
    
    rule "trait implied bound" prove_wc.rs:117 (failed: empty_collection)