Function bad_rule_k

crates/kernel/src/tutorial/defeq.rs:1177–1233

()

        "_",
        apps(
          cnst("Eq", &[usucc(uzero())]),
          &[cnst("Bool", &[]), cnst("Bool.true", &[]), var(0)],
        ),
        cnst("Bool", &[]),
      ),
    );
    let rec_app = apps(
      cnst("Eq.rec", &[usucc(uzero()), usucc(uzero())]),
      &[
        cnst("Bool", &[]),
        cnst("Bool.true", &[]),
        motive,
        var(0),                  // a
        cnst("Bool.false", &[]), // a' = false (doesn't match a = true)
        var(1),                  // h
      ],
    );

    let ty = npi(
      "h",
      tf_eq.clone(),
      npi(
        "a",
        cnst("Bool", &[]),
        eq_expr(usucc(uzero()), cnst("Bool", &[]), rec_app, var(0)),
      ),
    );

    let val = nlam(
      "h",
      tf_eq,
      nlam(
        "a",
        cnst("Bool", &[]),
        eq_refl_expr(usucc(uzero()), cnst("Bool", &[]), var(0)),
      ),
    );

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

  /// A conclusive Rule-K rejection must not be followed by normalization of
  /// the same major premise.  This is the small reducer shape behind the
  /// TauCeti `castLpₗᵢ` regression: the constructor candidate has already
  /// proved that the equality indices differ, while the propositional proof
  /// itself can be arbitrarily expensive to expose.
  #[test]
  fn rule_k_reject_skips_expensive_major_whnf() {
    let mut env = eq_inductive_env();

    let tf_eq = apps(
      cnst("Eq", &[usucc(uzero())]),
      &[cnst("Bool", &[]), cnst("Bool.true", &[]), cnst("Bool.false", &[])],
    );
    let (impossible_id, impossible) =
      mk_axiom("impossibleEq", 0, vec![], tf_eq.clone());