Function cheap_beta_nested_bvar_picks_outer_arg

crates/kernel/src/subst.rs:1253–1266

()

    let fv1 = AE::fvar(FVarId(1), ());
    // Two binders peeled → Var(3) shifts down to Var(1)
    let result = instantiate_rev(&mut env, &v3, &[fv0, fv1]);
    assert_eq!(result, AE::var(1, ()));
  }

  #[test]
  fn instantiate_rev_under_inner_binder() {
    let mut env = InternTable::<Anon>::new();
    let nat = AE::cnst(KId::new(mk_addr("Nat"), ()), Box::new([]));
    let v0 = AE::var(0, ()); // bound by inner λ
    let v1 = AE::var(1, ()); // refers to outer (the peeled binder at depth 0)
    let inner = AE::app(v0, v1);
    let lam = AE::lam((), (), nat.clone(), inner);
    let fv0 = AE::fvar(FVarId(0), ());
    let result = instantiate_rev(&mut env, &lam, std::slice::from_ref(&fv0));
    // Inside the lambda, Var(0) is still bound, Var(1) becomes fv0.
    let expected = AE::lam((), (), nat, AE::app(AE::var(0, ()), fv0));
    assert_eq!(result, expected);