Function good_fun_eta_dep

crates/kernel/src/tutorial/defeq.rs:171–217

()

  /// funEtaDep : ∀ (α : Type) (β : α → Type) (f : ∀ a, β a), (fun a => f a) = f
  #[test]
  fn good_fun_eta_dep() {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

    // At depth 3: f=var(0), β=var(1), α=var(2)
    // f : ∀ (a : α), β a. At depth 2: α=var(1), β=var(0)
    // f_ty = ∀ (a : α), β a = npi("a", var(1), app(var(1), var(0)))
    // Inside f_ty pi: a=var(0), β=var(1), α=var(2). β a = app(var(1), var(0))
    let f_ty = npi("a", var(1), app(var(1), var(0)));

    // eta_lhs = fun a => f a. At depth 3: α=var(2), f=var(0)
    // lambda domain: α at depth 3 = var(2)
    // Inside lambda (depth 4): a=var(0), f=var(1), β=var(2), α=var(3)
    let eta_lhs = nlam("a", var(2), app(var(1), var(0)));

    // ∀ a, β a at depth 3 (for Eq type arg):
    // npi("a", var(2), app(var(2), var(0))) — inside pi: β shifts from 1→2
    let pi_ty = npi("a", var(2), app(var(2), var(0)));

    // Eq.{1} (∀ a, β a) (fun a => f a) f
    let eq_app = eq_expr(usucc(uzero()), pi_ty.clone(), eta_lhs, var(0));

    // β : α → Type. At depth 1: α = var(0). β_ty = npi("a", var(0), sort1())
    // But β is NOT the pi type, it's a variable of type α → Type
    let beta_ty = pi(var(0), sort1()); // α → Type (non-dependent arrow)

    let ty = npi(
      "α",
      sort1(),
      npi("β", beta_ty.clone(), npi("f", f_ty.clone(), eq_app)),
    );

    // fun α β f => Eq.refl.{1} (∀ a, β a) f
    let val = nlam(
      "α",
      sort1(),
      nlam(
        "β",
        beta_ty,
        nlam("f", f_ty, eq_refl_expr(usucc(uzero()), pi_ty, var(0))),
      ),
    );

    let (id, c) = mk_thm("funEtaDep", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  // ==========================================================================
  // Batch 10: Structure eta (Tutorial.lean line 967–968)