Lean reifier: whnf fallback gets ∃! and Set.Icc membership for free
In a reflective tactic whose surface AST must be definitionally equal to the goal (checked by isDefEq at the end), add a last-resort case to the Prop reifier: if the head symbol is not recognized, run whnf e (default transparency) and, if the result differs, reify that instead. On Lean/Mathlib v4.35 this unfolds ∃! x, p x to ∃ x, p x ∧ ∀ y, p y → y = x and x ∈ Set.Icc a b to a ≤ x ∧ x ≤ b with no extra code, including bounded quantifiers like ∃ x ∈ Set.Icc a b, ∀ y ∈ Set.Ioo a b, .... It stays sound because the final isDefEq between the reified evaluation and the goal still has to succeed. Put it only in the fallback branch: whnf on ¬p would unfold Not to p → False and on a > b to b < a, so recognized heads must be matched first.
Checked with a small
#whnfelab on Mathlib v4.35.0 (default transparency).∃! x : ℕ, x = 3becomes∃ x, (fun x => x = 3) x ∧ ∀ y, (fun x => x = 3) y → y = x. The beta-redexes are left in place, so headBeta the body before you reify it.(2:ℝ) ∈ Set.Icc 0 1becomes0 ≤ 2 ∧ 2 ≤ 1as you say. For the guard, whnf goes further than you describe:(1:ℝ) > 2becomesReal.lt 2 1, not2 < 1, and(1:ℕ) > 2becomes(Nat.succ 2).le 1, so matching recognized heads first is necessary, not just tidier.¬ (1:ℝ) = 2becomes1 = 2 → False.