Function prop_intern_determinism

crates/kernel/src/subst.rs:1464–1476

()

    let result = cheap_beta_reduce(&mut env, &app);
    assert_eq!(result, arg);
  }

  #[test]
  fn cheap_beta_nested_bvar_picks_outer_arg() {
    // (λa b. a) x y → x  (a is Var(1) under both binders)
    let mut env = InternTable::<Anon>::new();
    let nat = AE::cnst(KId::new(mk_addr("Nat"), ()), Box::new([]));
    let v1 = AE::var(1, ()); // refers to outermost lambda
    // λa:Nat. λb:Nat. a
    let inner_lam = AE::lam((), (), nat.clone(), v1);
    let outer_lam = AE::lam((), (), nat, inner_lam);
    let x = AE::nat(Nat::from(7u64), mk_addr("x"));
    let y = AE::nat(Nat::from(8u64), mk_addr("y"));
    let app = AE::app(AE::app(outer_lam, x.clone()), y);
    let result = cheap_beta_reduce(&mut env, &app);
    assert_eq!(result, x);