Function lam

crates/kernel/src/inductive.rs:4540–4542

Helper: build `λ (_ : a), b`

(a: AE, b: AE)

      .get_result_sort_level(&ty, u64_to_usize(ind_params + ind_indices)?)?;
    if !univ_eq(&result_level, &KUniv::zero()) {
      return Ok(false);
    }

    // 3. Exactly one constructor with zero non-param fields
    if ctors.len() != 1 {
      return Ok(false);