Documentation

InfinitaryLogic.Methods.Interpolation.QuotientTermModel

Deprecated re-export shim (issue #34 rehoming) #

The countable Henkin-completion kernel serves two arcs (#8 Craig interpolation, #12 well-ordering) and was rehomed to Methods/Henkin/CountableCompletion/QuotientTermModel.lean. This shim keeps the old import path working for at least one release; update imports to the new path. All declaration names and namespaces are unchanged.