Impossible intermediate_field.adjoin notation

[gebner]

Lean 3:

notation K`⟮`:std.prec.max_plus l:(foldr `, ` (h t, insert.insert t h) ∅) `⟯` := adjoin K l
lemma induction2 {α β γ : solvable_by_rad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ :=

Synport:

-- ./././Mathport/Syntax/Translate/Basic.lean:958:11: unsupported (impossible)
theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮⟯) (hα : P α) (hβ : P β) : P γ := by

[digama0]

I'm not certain (I can't figure out what notation it might be overlapping), but I believe this is will also be fixed by leanprover-community/lean#754 .