Function good_nat_lit_eq

crates/kernel/src/tutorial/reduction.rs:1004–1029

()

    let nat_3 = ME::nat(Nat::from(3u64), Address::hash(b"natval_3"));
    let succ_succ_succ_zero = app(
      cnst("N.succ", &[]),
      app(cnst("N.succ", &[]), app(cnst("N.succ", &[]), cnst("N.zero", &[]))),
    );

    // Eq.{1} N 3 (succ (succ (succ zero)))
    let ty = eq_expr(usucc(uzero()), nat(), nat_3.clone(), succ_succ_succ_zero);
    // Eq.refl.{1} N 3
    let val = eq_refl_expr(usucc(uzero()), nat(), nat_3);

    let (id, c) = mk_thm("natLitEq", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    let mut prims = test_prims(&env);
    prims.nat = mk_id("N");
    prims.nat_zero = mk_id("N.zero");
    prims.nat_succ = mk_id("N.succ");
    check_accepts_with_prims(&mut env, &id, prims);
  }

  // ==========================================================================
  // Prod + projection reduction (Tutorial.lean 701–705, 902–903)
  // ==========================================================================

  /// Build Prod.{u,v} : Type u → Type v → Type (max u v) environment.
  fn prod_env() -> KEnv<Meta> {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

    // Also need Bool for projection tests
    let bool_id = mk_id("Bool");