Function pi

crates/kernel/src/inductive.rs:4530–4532

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

(a: AE, b: AE)

    }

    // 3. Exactly one constructor with zero non-param fields
    if ctors.len() != 1 {
      return Ok(false);
    }
    match self.try_get_const(&ctors[0])? {
      Some(KConst::Ctor { fields, .. }) => Ok(fields == 0),