Function mk_prop_structure_proj_test

crates/kernel/src/tutorial/defeq.rs:1891–1910

Helper: build test `name : PropStructure.{0,1} → resType := fun x => .proj PropStructure idx x`

(
    env: &mut KEnv<Meta>,
    name: &str,
    res_ty: ME,
    idx: u64,
  )

    );

    // Minimal recursor (Prop elimination only since it's a Prop structure)
    let ps_motive = pi(cnst("PropStructure", &[param(0), param(1)]), sort0());
    let ps_rec_ty = ipi(
      "motive",
      ps_motive,
      npi(
        "t",
        cnst("PropStructure", &[param(0), param(1)]),
        app(var(1), var(0)),
      ),
    );
    env.insert(
      ps_rec_id.clone(),
      KConst::Recr {
        name: mk_name("PropStructure.rec"),
        level_params: vec![mk_name("u"), mk_name("v")],
        k: false,
        is_unsafe: false,
        lvls: 2,
        params: 0,
        indices: 0,
        motives: 1,
        minors: 0,