[oxura]

Fixes #1623.

The translation expanded a stored function f to λx => f(x) when rebuilding a constructor. The dependent proof goal still contained f, and BendTT does not identify those terms by eta conversion.

Constructor fields now keep their original function values. Non-field argument translation and the Lean kernel are unchanged. The regression rebuilds a matched constructor and reuses a proof helper; the direct and original-value cases remain checked too.

Verified with the actual --verdict CLI: the new case and five existing eta/congruence/dependent-constructor examples all report ALL PROOFS CHECK. The repository gate passes 54/54. I did not run the macOS/Metal gate cluster.

Removed the GUIDE.md changes as requested in #1644.

[Lorenzobattistela]

Thanks for the fix. #1623's repro does check now, but the change breaks cases that pass --verdict on main.

Fields stop going η-long while arguments, equation sides and def bodies still do, so a function that reaches a field one way and an argument the other way no longer meets itself in the kernel:

• tests/check/ctr_param_field_eta.bend (from #1620) now fails --verdict at pair:

  expected: (keep λx1 => (x0 x1))
  observed: (.Tuple, (x0, ((.False, ()), ())))
  

  The safe gate goes from 0 to 1 false reject on main 8f86f73.
• A helper g(f: Type -> Type) -> {Box{f} == Box{f} : Box} called as g(f).
• Unfolding a def that builds the constructor: {k(f) == Box{f} : Box} with k(f) = Box{f}, and the same with Base's Some{f}.
• A rewrite %e by e : {f == g : Type -> Type} into a motive with the function in a field.
• η-equal fields: {Box{f} == Box{x => f(x)} : Box}, and mk() == FB{n => id(n)} with mk() = FB{id}.

All of these pass --check-only, and pass --verdict on main.

Also:

• The title says "neutral" fields, but the flag skips every field value that isn't a λ, including def names and partial applications.
• arg_term's comment still says arguments go η-long because they may reach a type. That applies to fields too.
• The new test only covers the match-and-rebuild direction. Please add the cases above.

[oxura]

You're right — skipping fields was too broad. I'm reworking the normalization so fields and arguments agree, and adding these cases before asking for another look.

[oxura]

The field-only normalization is not safe: it makes valid field/argument equalities fail. I’m withdrawing this version rather than asking you to merge a regression. #1623 still needs a normalization change that handles both positions consistently. Thanks for the counterexamples.