Lambda-lifting as a tableau α-rule.

Walks a term and, for every closed lambda subterm that occurs as an argument of a non-logical rigid constant, replaces the abstraction with a fresh constant c of the same arrow type and emits a typed-equality axiom c =_τ λx̄. body. The axiom is a normal branch formula — the :equality_expansion rule on typed_equality (Rules.classify_formula/1) decomposes it via extensional_equality / leibniz_equality, so subsequent reasoning rides on the standard γ/α/atomic/paramodulation pipeline.

Importantly, lift constants are not added to branch.defs; they cannot be undone by Semantics.unfold_defs!. Definition unfolding and lambda lifting therefore do not interact.

η-expansions of named constants (e.g. λx. f(x) for a constant f of arrow type) are skipped: lifting them would be useless indirection.