Function good_and_left

crates/kernel/src/tutorial/defeq.rs:1515–1546

()

      "motive",
      pi(nat(), sort(param(0))),
      npi("t", nat(), app(var(1), var(0))),
    );
    env.insert(
      rec_id.clone(),
      KConst::Recr {
        name: mk_name("N.rec"),
        level_params: vec![mk_name("u")],
        k: false,
        is_unsafe: false,
        lvls: 1,
        params: 0,
        indices: 0,
        motives: 1,
        minors: 0,
        block: block_id.clone(),
        member_idx: 0,
        ty: rec_ty,
        rules: vec![],
        lean_all: vec![block_id.clone()],
      },
    );
    env.blocks.insert(block_id, vec![mk_id(n), zero_id, succ_id, rec_id]);

    // type: N → N, value: fun x => .proj N 0 x
    let ty = pi(nat(), nat());
    let val = nlam("x", nat(), ME::prj(mk_id("N"), 0, var(0)));
    let (id, c) = mk_defn(
      "projNotStruct",
      0,
      vec![],
      ty,
      val,
      ix_common::env::ReducibilityHints::Opaque,
    );
    env.insert(id.clone(), c);