Function good_bool_rec_reduction

crates/kernel/src/tutorial/reduction.rs:393–425

()

    let mut env = bool_env();

    // Test: Bool.rec (motive := fun _ => Bool) Bool.false Bool.true Bool.false = Bool.false
    // i.e., the recursor on false returns the false-case value
    //
    // ∀ {motive : Bool → Sort 1} (hf : motive Bool.false) (ht : motive Bool.true),
    //   Eq.{1} (motive Bool.false) (Bool.rec hf ht Bool.false) hf
    //
    // Simplified: test with concrete motive = fun _ => Bool
    let motive = nlam("_", cnst("Bool", &[]), cnst("Bool", &[])); // fun _ => Bool
    let rec_app = apps(
      cnst("Bool.rec", &[usucc(uzero())]),
      &[
        motive.clone(),
        cnst("Bool.false", &[]), // false case returns Bool.false
        cnst("Bool.true", &[]),  // true case returns Bool.true
        cnst("Bool.false", &[]), // major: false
      ],
    );
    // After reduction: Bool.rec ... false = false-case = Bool.false
    let ty = eq_expr(
      usucc(uzero()),
      cnst("Bool", &[]),
      rec_app,
      cnst("Bool.false", &[]),
    );
    let val =
      eq_refl_expr(usucc(uzero()), cnst("Bool", &[]), cnst("Bool.false", &[]));
    let (id, c) = mk_thm("boolRecFalse", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  /// Bool.rec on true returns the true-case value
  #[test]
  fn good_bool_rec_reduction_true() {
    let mut env = bool_env();