The thought was to try to define the ternary P [c]⊸ N ("P implies N if c is in the context right now") by staring at the translation clause

`(P ⊸ N) @ f = ∃αφ.(f = α⊸φ) ⊗ (P @ α) ⊗ (N @ φ)`

and modify it to be

`(P [c]⊸ N) @ f = ∃αβφ.(f = α⊸β⊸φ) ⊗ (P @ α) ⊗ (c @ β) ⊗ (N @ β ⊸ φ)`

But then if you try to prove that focusing holds, you come to a case like ↓(P [c]⊸ ↑↓N) and you can't contort

(↓(P [c]⊸ ↑↓N)) @ r = ∀θ.(P [c]⊸ ↑↓N) @ θ ⇒ (r ▷ θ)

= ∀θ.(∃αβφ.(θ = α⊸β⊸φ) ⊗ (P @ α) ⊗ (c @ β) ⊗ (↑↓N @ β ⊸ φ)) ⇒ (r ▷ θ)

⊣⊢ ∀αβφ. (P @ α) ⇒ (c @ β) ⇒ (↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)

in any way to make the ↑↓N situated in a ↓↑↓N so you can Brouwer's-theorem it down to ↓N. It's

**exactly**the (c @ β) preventing you from narrowing the scope of the ∀βφ like

∀α (P @ α) ⇒ (c @ β) ⇒ ∀βφ. (↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)

and observing that

∀βφ.(↑↓N @ β ⊸ φ) ⇒ (r ▷ α⊸β⊸φ)

⊣⊢ ∀φ.(↑↓N @ φ) ⇒ (r ⊗ α ▷ φ)

= (↓↑↓N) @ (r ⊗ α)

⊣⊢ (↓N) @ (r ⊗ α)

So the best we can do is a ternary connective (P1 [c]⊸ P2) which can't focus through P2. But if you unpack the definition of this and look at the resulting inference rules, SPOILER ALERT, it works essentially the same way as

c ⊸ P1 ⊸ ↑(c ⊗ P2)

Which is the same ol' boring take-and-put-back semantics we were trying to avoid! Boo.