Function bad_proj_out_of_range

crates/kernel/src/tutorial/defeq.rs:1380–1403

()

    let minor_r =
      npi("left", var(3), npi("right", var(3), app(var(2), mk_app_r)));
    let rule_rhs = nlam(
      "a",
      sort0(),
      nlam(
        "b",
        sort0(),
        nlam(
          "motive",
          motive_ty_r,
          nlam(
            "intro_case",
            minor_r,
            nlam(
              "left",
              var(3),
              nlam("right", var(3), app(app(var(2), var(1)), var(0))),
            ),
          ),
        ),
      ),
    );

    env.insert(
      rec_id.clone(),
      KConst::Recr {
        name: mk_name("And.rec"),
        level_params: vec![mk_name("u")],