Function bad_non_prop_eq

crates/kernel/src/tutorial/defeq.rs:251–279

()

  /// ∀ (α : Type) (a b : α), Eq a b
  #[test]
  fn bad_non_prop_eq() {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

    // ∀ (α : Type) (a b : α), Eq.{1} α a b
    // depth 3: α=var(2), a=var(1), b=var(0)
    let ty = npi(
      "α",
      sort1(),
      npi(
        "a",
        var(0),
        npi("b", var(1), eq_expr(usucc(uzero()), var(2), var(1), var(0))),
      ),
    );
    // fun α a b => Eq.refl.{1} α a  (claims Eq a a, but type says Eq a b — no proof irrel for Type)
    let val = nlam(
      "α",
      sort1(),
      nlam(
        "a",
        var(0),
        nlam("b", var(1), eq_refl_expr(usucc(uzero()), var(2), var(1))),
      ),
    );
    let (id, c) = mk_thm("badNonPropEq", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    check_rejects(&mut env, &id);
  }

  // ==========================================================================
  // Batch 12: Unit eta (Tutorial.lean 958–965)