pub fn defeq_for_test(ctx: &Context, a: &Term, b: &Term) -> bool
Definitional equality of two terms — exposed for tests that pin conversion behaviour (structure eta, proof irrelevance) directly.