no goals
ι : Sort ?u.22270
α : Sort ?u.22275
κ : ι → Sort ?u.22272
p✝ q✝ : α → Prop
q : Prop
p : α → Prop
inst✝ : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
simp [or_comm, Decidable.forall_or_left]