English
Transform a formula by existentially quantifying over Sum.inr variables and imposing a uniqueness condition on the solutions.
Русский
Преобразование формулы путём существования по Sum.inr и требования уникальности решений.
LaTeX
$$$\\text{iExsUnique} : [Finite\\; β] \\to (\\phi: L.Formula (α \\oplus β) \\to L.Formula α)$$$
Lean4
/-- `iExsUnique f φ` transforms a `L.Formula (α ⊕ β)` into a `L.Formula α` by existentially
quantifying over all variables `Sum.inr _` and asserting that the solution should be unique -/
noncomputable def iExsUnique [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formula α :=
iExs β <|
φ ⊓
iAlls β
((φ.relabel (fun a => Sum.elim (.inl ∘ .inl) .inr a)).imp <|
.iInf fun g => Term.equal (var (.inr g)) (var (.inl (.inr g))))
