| 4818 | if stt |
| 4819 | .below_call_site_plans |
| 4820 | .get(&below_name) |
| 4821 | .is_some_and(|existing| *existing != new_plan) |
| 4822 | { |
| 4823 | return Err(CompileError::InvalidMutualBlock { |
| 4824 | reason: format!( |
| 4825 | "conflicting below call-site plans for '{}' — two blocks \ |
| 4826 | claim one source-indexed aux name", |
| 4827 | below_name.pretty(), |
| 4828 | ), |
| 4829 | }); |
| 4830 | } |
| 4831 | // Prop-level (IndPredBelow) `.below` is an INDUCTIVE, so user |
| 4832 | // code can also reference its constructors and its |
| 4833 | // `.casesOn` wrapper — both start with the below params |
| 4834 | // (parent params + parent motives) and need the same motive |
| 4835 | // permutation. Registered under their own names in the same |
| 4836 | // map; the apply site discriminates the telescope shape via |
| 4837 | // `below_plan_key_is_head`. `X.below.rec` is deliberately |
| 4838 | // not registered (only regenerated wrappers reference it, |
| 4839 | // and those skip surgery via the aux-regen guard). |
| 4840 | let mut family_names: Vec<Name> = Vec::new(); |