Function poly_nested_flat_block

crates/kernel/src/inductive.rs:5514–5533

()

    );
    let cons_ty = pi(
      AE::sort(param(0)),
      pi(
        var(0),
        pi(
          app(cnst("List", &[param(0)]), var(1)),
          app(cnst("List", &[param(0)]), var(2)),
        ),
      ),
    );
    env.insert(
      mk_id("List.cons"),
      KConst::Ctor {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 1,
        induct: mk_id("List"),
        cidx: 1,
        params: 1,
        fields: 2,
        ty: cons_ty,
      },
    );