Function bad_eta_rule_k

crates/kernel/src/tutorial/defeq.rs:2009–2078

()

    let res_ty_inner = apps(
      cnst("Eq", &[usucc(uzero())]),
      &[cnst("PUnit", &[usucc(uzero())]), proj3.clone(), proj3],
    );
    // But this res_ty is inside the pi binder (at depth 1 where x=var(0))
    // The helper mk_prop_structure_proj_test wraps it in pi(PS, res_ty)
    // so res_ty should reference var(0) for x. But var(0) inside pi body
    // IS x. The .proj expressions use var(0) = x. Good.
    let id =
      mk_prop_structure_proj_test(&mut env, "projProp5", res_ty_inner, 4);
    check_rejects(&mut env, &id);
  }

  /// projProp6 (bad): idx=5, aFinalProof : PUnit.{0} — after dependent data
  #[test]
  fn bad_proj_prop6() {
    let mut env = prop_structure_env();
    let id = mk_prop_structure_proj_test(
      &mut env,
      "projProp6",
      cnst("PUnit", &[uzero()]),
      5,
    );
    check_rejects(&mut env, &id);
  }

  // ==========================================================================
  // etaRuleK corner case (Tutorial.lean 987–999)
  //
  // Partially applied Eq.rec with rule K should NOT trigger eta expansion.
  // @Eq.rec Bool true (fun _ _ => Bool) (a (Eq.refl true)) _ ≠ a
  // even though Eq.rec could reduce via Rule K if fully applied.
  // ==========================================================================

  /// etaRuleK: ∀ (a : true = true → Bool),
  ///   @Eq (true = true → Bool) (Eq.rec (fun _ _ => Bool) (a (Eq.refl true)) _) a
  /// BAD: partially applied recursor should not eta-expand to match `a`.
  #[test]
  fn bad_eta_rule_k() {
    let mut env = eq_inductive_env();

    let u1 = usucc(uzero());
    let bool_ty = cnst("Bool", &[]);

    // true = true
    let tt_eq = apps(
      cnst("Eq", std::slice::from_ref(&u1)),
      &[bool_ty.clone(), cnst("Bool.true", &[]), cnst("Bool.true", &[])],
    );

    // (true = true → Bool) — the type of `a`
    let a_ty = pi(tt_eq.clone(), bool_ty.clone());

    // motive for Eq.rec: fun _ _ => Bool
    let motive = nlam(
      "_",
      bool_ty.clone(),
      nlam(
        "_",
        apps(