forall commutes with or

Stream: new members

[Raphael Appenzeller]

I would like to use the following statement in a proof. I would have expected this to be in the library somewhere but library_search was not successful. Is there a different version that I could use, or should this be added to the library?

lemma logic_helper (α β : Type*) (A : α → Prop ) (B : β → Prop): (∀ u : α , ∀ v : β , A u ∨ B v )
                                                          ↔ (∀ u : α, A u) ∨ (∀ v : β , B v ) :=
begin
  sorry,
end

[Ruben Van de Velde]

lemma logic_helper (α β : Type*) (A : α → Prop ) (B : β → Prop): (∀ u : α , ∀ v : β , A u ∨ B v )
                                                          ↔ (∀ u : α, A u) ∨ (∀ v : β , B v ) :=
begin
  simp_rw [←forall_or_distrib_right, ←forall_or_distrib_left],
end