Custard: fold projections of a let-bound constructor

[gebner]

Fixes #4548.

let (a, (b, _)) = p in an inline_for_extraction callee left the caller building a tuple, naming it and reading it back out:

uint32_t LetPatFold_entry(uint32_t x) {
  FStar_Pervasives_Native_tuple2__uint32_tuple2_uint32_unit _letpattern =
      (FStar_Pervasives_Native_tuple2__uint32_tuple2_uint32_unit){
          ._1 = x,
          ._2 = (FStar_Pervasives_Native_tuple2__uint32_unit){ ._1 = (x + 1) } };
  return (_letpattern._1 + _letpattern._2._1);
}

Now it is return (x + (x + 1));.

The rewrites were already there -- iota on a match over a constructor, unbuild on a projection out of one -- but F* names the scrutinee first (let _letpattern = Mktuple2 ... in match _letpattern with ...), so neither ever sees a constructor.

• reduce's ELet case substitutes a let-bound constructor when every occurrence is destructed on the spot (the scrutinee of a match, or the target of a projection) and every field is reeval.
• unbuild does the same for the projection-only shape that depat leaves behind, using psub plus a guard that the body does not rebind the name.
• reeval is the condition the immediate case never needed: a field that is read moves, possibly more than once and possibly into a loop, so it is restricted to the bounded, allocation-free class -- variables, constants, projections, casts, coercions, tag reads, operators, and constructors over them. A call or an allocation keeps its binding, which is the issue's own caveat about discarded components. Constructors have to be in it or the rule does not fire on the nested tuple it was written for.

No declared type changes: the one-field struct a unit tail leaves is still declared, it is just no longer built.

Documented in section 129 of doc/ref/custard.md. New regression test tests/custard/pulse/LetPatFold.fst. The full gate is green and no goldens moved.