Function good_rtree_rec_reduction

crates/kernel/src/tutorial/reduction.rs:902–971

()

    //     (fun children _ih => children true) t
    let motive = nlam("_", rt(), rt());
    let leaf_case = cnst("RTree.leaf", &[]);
    // node case: fun children ih => children Bool.true
    // depth 2: ih=var(0), children=var(1)
    let ih_ty = npi("b", cnst("Bool", &[]), rt()); // simplified: ∀ b, RTree
    let node_case = nlam(
      "children",
      pi(cnst("Bool", &[]), rt()),
      nlam("_ih", ih_ty, app(var(1), cnst("Bool.true", &[]))),
    );

    let left_val = nlam(
      "t",
      rt(),
      apps(
        cnst("RTree.rec", &[usucc(uzero())]),
        &[motive, leaf_case, node_case, var(0)],
      ),
    );
    let (left_id, left_c) = mk_defn(
      "RTree.left",
      0,
      vec![],
      pi(rt(), rt()),
      left_val,
      ReducibilityHints::Abbrev,
    );
    env.insert(left_id, left_c);

    // Test: ∀ (t1 t2 : RTree), (RTree.node (Bool.rec t2 t1)).left = t1
    // Bool.rec.{1} (fun _ => RTree) t2 t1 : Bool → RTree
    // Then RTree.node applied to this, then .left
    // depth 2: t1=var(1), t2=var(0)... wait, t1 first then t2:
    // ∀ (t1 : RTree) (t2 : RTree), ...
    // depth 2: t2=var(0), t1=var(1)
    let bool_rec_app = apps(
      cnst("Bool.rec", &[usucc(uzero())]),
      &[
        nlam("_", cnst("Bool", &[]), rt()), // motive: fun _ => RTree
        var(0),                             // false case = t2
        var(1),                             // true case = t1
      ],
    );
    // RTree.node (Bool.rec ...) : RTree
    let node_app = app(cnst("RTree.node", &[]), bool_rec_app);
    // RTree.left (RTree.node ...) should reduce to t1
    let lhs = app(cnst("RTree.left", &[]), node_app);
    let ty = npi(
      "t1",
      rt(),
      npi("t2", rt(), eq_expr(usucc(uzero()), rt(), lhs, var(1))),
    );
    let val = nlam(
      "t1",
      rt(),
      nlam("t2", rt(), eq_refl_expr(usucc(uzero()), rt(), var(1))),
    );

    let (id, c) = mk_thm("rtreeRecReduction", 0, vec![], ty, val);