Theorem: impliesOrImpliesGeneralized (NazgandLean4/Prop.lean)

State before:
k : ℕ+
p : ℕ → Prop
r : Prop
⊢ (∀ k₀ ∈ range ↑k, p k₀ → r) ↔ (∃ k₀ ∈ range ↑k, p k₀) → r
Tactic:
aesop
State after:
no goals