Function good_proj_red

crates/kernel/src/tutorial/reduction.rs:1266–1290

()

    // .proj Prod 1 pair = false
    let proj = ME::prj(mk_id("Prod"), 1, pair);
    // Eq.{1} Bool (.proj Prod 1 (mk true false)) false
    let ty =
      eq_expr(usucc(uzero()), cnst("Bool", &[]), proj, cnst("Bool.false", &[]));
    let val =
      eq_refl_expr(usucc(uzero()), cnst("Bool", &[]), cnst("Bool.false", &[]));

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

  /// structEta : ∀ (x : Prod Bool Bool), x = Prod.mk (.proj Prod 0 x) (.proj Prod 1 x)
  /// Structure eta: a value of a structure type equals the constructor applied to its projections.
  #[test]
  fn good_struct_eta() {
    let mut env = prod_env();

    let prod_bb = app(
      app(cnst("Prod", &[uzero(), uzero()]), cnst("Bool", &[])),
      cnst("Bool", &[]),
    );

    // depth 1: x=var(0) : Prod Bool Bool
    let proj0 = ME::prj(mk_id("Prod"), 0, var(0));
    let proj1 = ME::prj(mk_id("Prod"), 1, var(0));
    let reconstructed = apps(
      cnst("Prod.mk", &[uzero(), uzero()]),
      &[cnst("Bool", &[]), cnst("Bool", &[]), proj0, proj1],