Function good_prod_rec_reduction

crates/kernel/src/tutorial/reduction.rs:1329–1360

()

      &[
        cnst("Bool", &[]),
        cnst("Bool", &[]),
        cnst("Bool.true", &[]),
        cnst("Bool.false", &[]),
      ],
    );
    let rec_app = apps(
      cnst("Prod.rec", &[uzero(), uzero(), u1.clone()]),
      &[cnst("Bool", &[]), cnst("Bool", &[]), motive, f_case, pair],
    );
    let ty =
      eq_expr(u1.clone(), cnst("Bool", &[]), rec_app, cnst("Bool.true", &[]));
    let val = eq_refl_expr(u1, cnst("Bool", &[]), cnst("Bool.true", &[]));

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

  // ==========================================================================
  // Quotient tests (Tutorial.lean 1185–1224)
  // ==========================================================================

  /// Add Eq as a full inductive (not just axioms) — needed for Quot.lift validation.
  fn add_eq_inductive(env: &mut KEnv<Meta>) {
    let eq_id = mk_id("Eq");
    let refl_id = mk_id("Eq.refl");
    let eq_rec_id = mk_id("Eq.rec");

    let eq_ty =
      ipi("α", sort(param(0)), npi("a", var(0), npi("b", var(1), sort0())));
    env.insert(
      eq_id.clone(),
      KConst::Indc {
        name: mk_name("Eq"),
        level_params: vec![mk_name("u")],