∀(a : Type) → ∀(f : {} → a) → ∀(ts : < Bar : {} | Baz : {} >) → a