Function good_struct_eta

crates/kernel/src/tutorial/reduction.rs:1295–1325

()

      &[cnst("Bool", &[]), cnst("Bool", &[]), proj0, proj1],
    );

    // ∀ (x : Prod Bool Bool), Eq.{1} (Prod Bool Bool) x (Prod.mk (x.1) (x.2))
    let ty = npi(
      "x",
      prod_bb.clone(),
      eq_expr(usucc(uzero()), prod_bb.clone(), var(0), reconstructed),
    );

    // fun x => Eq.refl.{1} (Prod Bool Bool) x
    let val =
      nlam("x", prod_bb.clone(), eq_refl_expr(usucc(uzero()), prod_bb, var(0)));

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

  /// prodRecEqns: Prod.rec f (Prod.mk true false) = f true false = true
  #[test]
  fn good_prod_rec_reduction() {
    let mut env = prod_env();
    let u1 = usucc(uzero());

    let prod_bb = app(
      app(cnst("Prod", &[uzero(), uzero()]), cnst("Bool", &[])),
      cnst("Bool", &[]),
    );
    let motive = nlam("_", prod_bb, cnst("Bool", &[]));
    let f_case =
      nlam("a", cnst("Bool", &[]), nlam("b", cnst("Bool", &[]), var(1)));
    let pair = apps(
      cnst("Prod.mk", &[uzero(), uzero()]),
      &[
        cnst("Bool", &[]),