Function good_bool_rec_reduction_true

crates/kernel/src/tutorial/reduction.rs:429–453

()

    let mut env = bool_env();

    let motive = nlam("_", cnst("Bool", &[]), cnst("Bool", &[]));
    let rec_app = apps(
      cnst("Bool.rec", &[usucc(uzero())]),
      &[
        motive,
        cnst("Bool.false", &[]),
        cnst("Bool.true", &[]),
        cnst("Bool.true", &[]), // major: true
      ],
    );
    let ty = eq_expr(
      usucc(uzero()),
      cnst("Bool", &[]),
      rec_app,
      cnst("Bool.true", &[]),
    );
    let val =
      eq_refl_expr(usucc(uzero()), cnst("Bool", &[]), cnst("Bool.true", &[]));
    let (id, c) = mk_thm("boolRecTrue", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  // ==========================================================================
  // Batch 16: Nat inductive + recursor reduction (Tutorial.lean 231, 710–718)
  // ==========================================================================

  /// Build N (Nat-like) environment with working recursor rules.