diff --git a/formality-core/SKILL.md b/formality-core/SKILL.md
new file mode 100644
index 0000000..c1e1abe
--- /dev/null
+++ b/formality-core/SKILL.md
@@ -0,0 +1,407 @@
+---
+name: formality-core
+description: Idiomatic patterns for writing code with formality-core (a-mir-formality). Use when writing or reviewing judgment functions, type definitions, or parser-related code in projects built on formality-core.
+crates: formality-core
+---
+
+# Idiomatic formality-core
+
+This skill covers patterns and anti-patterns when writing code with [formality-core](https://rust-lang.github.io/a-mir-formality/formality_core.html). Following these idioms produces cleaner, more concise code and avoids subtle bugs.
+
+## Generated constructors from `#[term]`
+
+The `#[term]` macro generates constructor methods on every type it annotates.
+
+### Structs get `::new(...)`
+
+```rust
+#[term($name $[?parameters])]
+pub struct NamedTy {
+    pub name: TypeName,
+    pub parameters: Parameters,
+}
+```
+
+Generates: `NamedTy::new(name, parameters)` where each parameter accepts `impl Upcast<FieldType>`.
+
+### Enums get `::snake_case_variant(...)`
+
+```rust
+#[term]
+pub enum Perm {
+    #[grammar(given_from $[v0])]
+    Mv(Set<Place>),
+    Given,
+    Shared,
+    #[grammar(ref $[?v0])]
+    Rf(Set<Place>),
+    #[grammar(mut $[v0])]
+    Mt(Set<Place>),
+    #[variable(Kind::Perm)]
+    Var(Variable),
+    Apply(Arc<Perm>, Arc<Perm>),
+}
+```
+
+Generates lowercase snake_case methods. Rust keywords get a trailing `_`:
+
+| Variant | Generated method |
+|---------|-----------------|
+| `Mv(Set<Place>)` | `Perm::mv(places)` |
+| `Given` | *(no method — zero fields)* |
+| `Shared` | *(no method — zero fields)* |
+| `Rf(Set<Place>)` | `Perm::rf(places)` |
+| `Mt(Set<Place>)` | `Perm::mt(places)` |
+| `Var(Variable)` | `Perm::var(v)` |
+| `Apply(Arc<Perm>, Arc<Perm>)` | `Perm::apply(p1, p2)` |
+
+Zero-field variants (like `Given`, `Shared`) get **no** generated constructor — use the enum literal `Perm::Given` directly.
+
+#### Rule: always prefer generated constructors
+
+```rust
+// ✅ Good — generated constructor, accepts impl Upcast
+Perm::var(perm_var)
+Perm::rf(set![place])
+NamedTy::new(name, substitution)
+Predicate::parameter(ParameterPredicate::Copy, perm_var)
+
+// ❌ Bad — manual construction, requires explicit conversion
+Perm::Var(perm_var.upcast())
+Perm::Var(Variable::from(perm_var.clone()))
+Perm::Rf(set![place.clone()])
+```
+
+The generated constructors accept `impl Upcast<T>` for every field, so they handle conversions (e.g., `UniversalVar` → `Variable` → `Perm::Var`) and cloning automatically. You never need to manually `.upcast()`, `.into()`, or `.clone()` when calling a generated constructor.
+
+## Upcast coercions: avoiding explicit clones
+
+The `Upcast`/`UpcastFrom` system provides automatic coercions. The key blanket impl:
+
+```rust
+impl<T: Clone, U> UpcastFrom<&T> for U where U: UpcastFrom<T> { ... }
+```
+
+This means: **anywhere `impl Upcast<T>` is expected, you can pass `&T` and it will clone for you.** This eliminates most explicit `.clone()` calls.
+
+### Where this applies
+
+1. **Generated constructors** — all parameters accept `impl Upcast<FieldType>`
+2. **`judgment_fn!` parameters** — the function signature is `fn f(x: impl Upcast<T>)`
+3. **`Env` methods** — `push_local_variable`, `add_assumptions`, etc. accept `impl Upcast<T>`
+4. **Judgment return positions** — results upcast automatically to the declared return type
+
+### Common coercion chains
+
+| Source | Target | How |
+|--------|--------|-----|
+| `&T` | `T` | auto-clone via `UpcastFrom<&T>` |
+| `UniversalVar` | `Variable` | `UpcastFrom` |
+| `UniversalVar` | `Parameter` | via `Variable` → `Parameter` |
+| `NamedTy` | `Ty` | `UpcastFrom` on `Ty::NamedTy` variant |
+| `Ty` | `Parameter` | `UpcastFrom` on `Parameter::Ty` variant |
+| `Perm` | `Parameter` | `UpcastFrom` on `Parameter::Perm` variant |
+| `Place` | via `Var` | `UpcastFrom<Var> for Place` |
+| `Vec<T>` | `Vec<U>` | element-wise upcast |
+| `&[T]` | `Vec<U>` | element-wise upcast |
+
+### Upcasted iterator adapter
+
+Use `.upcasted()` (from `formality_core::Upcasted`) for element-wise upcast in iterator chains:
+
+```rust
+// ✅ Good
+let perms: Vec<Perm> = chains.into_iter().upcasted().collect();
+
+// ❌ Verbose
+let perms: Vec<Perm> = chains.into_iter().map(|c| c.upcast()).collect();
+```
+
+### Examples
+
+```rust
+// ✅ Good — pass &reference, upcast handles cloning
+let env = env.push_local_variable(Var::This, &class_ty)?;
+Predicate::parameter(ParameterPredicate::Copy, &perm_var)
+
+// ❌ Bad — unnecessary explicit clone
+let env = env.push_local_variable(Var::This, class_ty.clone())?;
+Predicate::parameter(ParameterPredicate::Copy, perm_var.clone())
+```
+
+**Exception:** When the value is already owned and you're done with it, just pass it directly — no `&` needed:
+
+```rust
+// ✅ Good — class_ty is owned and consumed here
+let env = env.push_local_variable(Var::This, class_ty)?;
+```
+
+## `judgment_fn!` patterns
+
+### Parameters are owned inside the body
+
+The macro expands `fn f(x: impl Upcast<T>)` and immediately does `let x: T = Upcast::upcast(x)`. Inside the rule body, `x` is an **owned `T`**. However, within pattern-matched destructuring, fields from a matched struct/enum are **references** (standard Rust match ergonomics).
+
+```rust
+judgment_fn! {
+    fn check(env: Env, decl: ClassDecl) => () {
+        (
+            // `decl` is owned ClassDecl
+            // After destructuring, `name` is `&ValueId`, `binder` is `&Binder<...>`
+            (let ClassDecl { name, binder, .. } = decl)
+            // But generated constructors accept `impl Upcast<T>`,
+            // which includes `&T`, so this just works:
+            (let class_ty = NamedTy::new(name, substitution))  // ✅ name is &ValueId, auto-cloned
+            ...
+        )
+    }
+}
+```
+
+### Pattern matching in conclusions for dispatch
+
+Use pattern matching in the conclusion to dispatch on variants — cleaner than `if` guards:
+
+```rust
+// ✅ Good — pattern match directly
+(
+    (let env = env.push_local_variable(Var::This, class_ty)?)
+    ...
+    ----------------------------------- ("given_class_drop")
+    (check_drop_body(class_ty, ClassPredicate::Given, env, body) => ())
+)
+
+(
+    ...
+    ----------------------------------- ("share_class_drop")
+    (check_drop_body(class_ty, ClassPredicate::Share | ClassPredicate::Shared, env, body) => ())
+)
+
+// ❌ Avoid — if-guard when pattern match works
+(
+    (if *class_predicate == ClassPredicate::Given)
+    ...
+    ----------------------------------- ("given_class_drop")
+    (check_drop_body(class_ty, class_predicate, env, body) => ())
+)
+```
+
+### Struct patterns in conclusions
+
+Destructure structs directly in the conclusion instead of matching a wrapper and then destructuring with `let`:
+
+```rust
+// ✅ Good — destructure in conclusion, result auto-upcasts
+(
+    (normalize_params(env, parameters) => norm_params)
+    --- ("named")
+    (normalize_ty(env, NamedTy { name, parameters }) => NamedTy::new(name, norm_params))
+)
+
+// ❌ Verbose — extra let + explicit wrapping
+(
+    (let NamedTy { name, parameters } = named_ty)
+    (normalize_params(env, parameters) => norm_params)
+    --- ("named")
+    (normalize_ty(env, Ty::NamedTy(named_ty))
+        => Ty::NamedTy(NamedTy { name: name.clone(), parameters: norm_params.to_vec() }))
+)
+```
+
+Note: `NamedTy::new(name, norm_params)` returns a `NamedTy`, which auto-upcasts to `Ty` (via the `Ty::NamedTy` variant cast) when the judgment's return type is `Ty`.
+
+### Upcast in return values
+
+Judgment results upcast to the declared return type automatically. If your judgment returns `Parameter`, you can return a `Ty` or `Perm` directly:
+
+```rust
+// ✅ Good — Ty auto-upcasts to Parameter
+(
+    (normalize_ty(env, ty) => norm_ty)
+    --- ("ty")
+    (normalize_param(env, Parameter::Ty(ty)) => norm_ty)
+)
+
+// ❌ Verbose — manual wrapping
+(
+    (normalize_ty(env, ty) => norm_ty)
+    --- ("ty")
+    (normalize_param(env, Parameter::Ty(ty)) => Parameter::ty(norm_ty))
+)
+```
+
+### Building collections with `Cons` and `()`
+
+For recursive list/set processing in judgments, use `Cons(head, tail)` in both pattern matching and return positions. Use `()` for empty collections.
+
+```rust
+judgment_fn! {
+    fn process_list(env: Env, items: Vec<Item>) => Vec<Item> {
+        // Base case: empty → empty (() upcasts to empty Vec)
+        (
+            --- ("nil")
+            (process_list(_env, ()) => ())
+        )
+
+        // Recursive: Cons destructures the head, Cons builds the result
+        (
+            (transform(env, item) => new_item)
+            (process_list(env, rest) => new_rest)
+            --- ("cons")
+            (process_list(env, Cons(item, rest)) => Cons(new_item, new_rest))
+        )
+    }
+}
+```
+
+This works for both `Vec<T>` and `Set<T>`. No need for `prepend` helpers, `Vec::new()`, or `std::iter::once(...).chain(...).collect()`.
+
+### Cut points with `!`
+
+Place `!` after a condition to mark a **match commit point**. Rules that fail before the cut are excluded from error reports. Use cuts on guard conditions that definitively select or reject a rule:
+
+```rust
+// ✅ Good — cut prevents "empty_drop failed" noise in error messages
+(
+    (if drop_body.block.statements.is_empty())!
+    ----------------------------------- ("empty_drop")
+    (check_drop_body(_class_ty, _class_predicate, _env, drop_body) => ())
+)
+```
+
+Without the `!`, if the empty check passes but a later rule fails, error reports would unhelpfully include "empty_drop failed because condition was false" for non-empty bodies.
+
+**Complementary guards should both have cuts.** When two rules partition cases with a boolean check, put `!` on both:
+
+```rust
+// ✅ Good — both branches cut
+(
+    (if !needs_work(&value))!
+    --- ("no work needed")
+    (process(_env, value) => value)
+)
+
+(
+    (if needs_work(&value))!
+    (do_work(env, value) => result)
+    --- ("do work")
+    (process(env, value) => result)
+)
+```
+
+### `Arc<T>` gotcha
+
+Fields declared as `Arc<T>` become `&Arc<T>` when destructured (standard Rust). Calling `.clone()` gives you `Arc<T>`, **not `T`**. When passing to a judgment or generated constructor that accepts `impl Upcast<T>`, use `&**x` to get `&T` — the `UpcastFrom<&T>` blanket impl handles the clone:
+
+```rust
+// Inside a judgment rule where `inner_ty` is `&Arc<Ty>`:
+(some_judgment(env, &**inner_ty) => result)  // ✅ &**inner_ty is &Ty, upcast clones it
+(some_judgment(env, inner_ty.clone()) => result)  // ❌ Passes Arc<Ty>, not Ty
+```
+
+For non-Arc fields (e.g., `perm: &Perm` from `ApplyPerm(Perm, Arc<Ty>)`), just pass `perm` directly — `&Perm` upcasts to `Perm` automatically.
+
+### `for_all` vs `in`
+
+- `(x in collection)` — **existential**: there exists some `x` in `collection` that satisfies the remaining conditions
+- `(for_all(x in collection) (condition))` — **universal**: all `x` in `collection` must satisfy `condition`
+
+```rust
+// Check ALL fields
+(for_all(field in fields)
+    (check_field(env, field) => ()))
+
+// Find SOME method matching the name
+(MethodDecl { name: _, binder } in methods.into_iter().filter(|m| m.name == *method_name))
+```
+
+## Using judgment results outside `judgment_fn!`
+
+Judgment functions return `ProvenSet<T>`, not `T` or `Result<T>`. Inside `judgment_fn!` rules, the `=>` syntax handles this automatically. Outside, you must extract results explicitly:
+
+```rust
+// Check if a judgment succeeds (bool)
+prove_is_copy(&env, &param).is_proven()
+
+// Extract a single result (when exactly one is expected).
+// into_singleton() returns Result<(T, ProofTree), Box<FailedJudgment>>.
+// Box<FailedJudgment> is compatible with `?` in anyhow contexts — no map_err needed.
+let (result, _proof) = red_perm(&env, &live_after, &perm)
+    .into_singleton()?;
+
+// Get all results as a map
+let results = my_judgment(&env, &x)
+    .into_map()?;
+```
+
+**Common mistake:** calling `.is_ok()` on a `ProvenSet` — it doesn't have that method. Use `.is_proven()` instead.
+
+## Parser / grammar conventions
+
+### Kind keywords are lowercase
+
+formality-core parses `Kind` variants as their lowercase names. For a `Kind` enum with `Ty` and `Perm` variants, the parser keywords are `ty` and `perm`:
+
+```rust
+// ✅ Correct in test strings / parsed programs
+"class Wrapper[ty T] { ... }"
+"class Foo[perm P, ty T] { ... }"
+
+// ❌ Wrong — "type" is not a keyword
+"class Wrapper[type T] { ... }"
+```
+
+### KEYWORDS vs grammar keywords
+
+Words in the `KEYWORDS` list in `declare_language!` are **globally reserved** — they can never be used as identifiers anywhere. Grammar keywords (`#[grammar(x)]` on enum variants) work without being in KEYWORDS — they're only recognized in the specific parsing context.
+
+**Only add to KEYWORDS when you want to block identifier use.** Don't add a word to KEYWORDS just because it appears in a `#[grammar(...)]` annotation.
+
+### Prefix ambiguity
+
+If one variant's keyword is a prefix of another's in the same enum (e.g., `given` vs `given_from[...]`), the parser silently matches the shorter one. Use distinct keywords to avoid this.
+
+### `$?` for optional fields
+
+`$?field` in a grammar annotation makes the field optional. The field type must implement `Default`. When the field is absent in the input, the `Default` value is used:
+
+```rust
+#[term($:where $,predicates { $*fields $*methods $?drop_body })]
+pub struct ClassDeclBoundData {
+    pub predicates: Vec<Predicate>,
+    pub fields: Vec<FieldDecl>,
+    pub methods: Vec<MethodDecl>,
+    pub drop_body: DropBody,  // Default::default() when omitted
+}
+```
+
+## Generated constructor name collisions
+
+The `#[term]` macro generates `EnumName::snake_case_variant(...)` for each variant. For example, `Perm::Or(Set<Perm>)` generates `Perm::or(...)`. If you add a hand-written method with the same name in an `impl` block, you get a **"duplicate definitions"** error. Use a distinct name:
+
+```rust
+// ❌ Fails — collides with generated Perm::or()
+impl Perm {
+    pub fn or(perms: impl IntoIterator<Item = Perm>) -> Perm { ... }
+}
+
+// ✅ Good — distinct name
+impl Perm {
+    pub fn flat_or(perms: impl IntoIterator<Item = Perm>) -> Perm { ... }
+}
+```
+
+## Summary of rules
+
+1. **Use generated constructors** (`Perm::var(x)` not `Perm::Var(x.upcast())`)
+2. **Pass references** where `impl Upcast<T>` is expected — the framework clones for you
+3. **Pattern match** in judgment conclusions instead of `if` guards
+4. **Destructure structs** in conclusions, not with separate `let` bindings
+5. **Let upcast handle return values** — `norm_ty` auto-upcasts to `Parameter`, `NamedTy` to `Ty`
+6. **Use `Cons`/`()` for collections** in judgment return positions, not manual Vec building
+7. **Use `!` cuts** on guard conditions, including both sides of complementary pairs
+8. **Use `&**x`** for `Arc<T>` fields, not `.clone()`
+9. **Use `ty`/`perm`** as kind keywords in parsed strings, not `type`/`perm`
+10. **Use `.into_singleton()?`** directly — no `map_err` needed
+11. **Use `.upcasted()`** for element-wise iterator upcast
+12. **Don't add to KEYWORDS** unless you need to reserve the word globally