| 1348 | // Open: peel the outer binder around body... actually body itself is a |
| 1349 | // lambda (the outer binder), and its inner is what we want to peel. |
| 1350 | // For simplicity, treat `body` directly as a body under one peeled |
| 1351 | // outer binder, then peel its inner lambda manually. |
| 1352 | let opened_outer = |
| 1353 | instantiate_rev(&mut env, &body, std::slice::from_ref(&fv_outer)); |
| 1354 | // opened_outer is now: λ(Nat). App(#0, fv_outer) |
| 1355 | let inner_body = match opened_outer.data() { |
| 1356 | ExprData::Lam(_, _, _, b, _) => b.clone(), |
| 1357 | _ => unreachable!(), |
| 1358 | }; |
| 1359 | let opened_inner = |
| 1360 | instantiate_rev(&mut env, &inner_body, std::slice::from_ref(&fv_inner)); |