Function good_unit_eta

crates/kernel/src/tutorial/defeq.rs:379–405

()

    let mut env = unit_env();
    // ∀ (x y : MyUnit), Eq.{1} MyUnit x y
    let ty = npi(
      "x",
      cnst("MyUnit", &[]),
      npi(
        "y",
        cnst("MyUnit", &[]),
        eq_expr(usucc(uzero()), cnst("MyUnit", &[]), var(1), var(0)),
      ),
    );
    // fun x y => Eq.refl.{1} MyUnit x
    // Kernel uses structure eta: x = MyUnit.star = y
    let val = nlam(
      "x",
      cnst("MyUnit", &[]),
      nlam(
        "y",
        cnst("MyUnit", &[]),
        eq_refl_expr(usucc(uzero()), cnst("MyUnit", &[]), var(1)),
      ),
    );
    let (id, c) = mk_thm("unitEta", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  // ==========================================================================
  // Acc inductive + reduction (Tutorial.lean 1161–1181)
  // ==========================================================================

  /// Build Acc inductive environment.