theorem CFGPDAEquiv.cfl_iff_pda_recognizes {α : Type u} (A : Language α) : A.IsContextFree ↔ ∃ (σ : Type u) (γ : Type u) (M : PDA α σ γ), M.language = A

Sipser, Lecture 4 (Equivalence of CFGs and PDAs). A language A is context-free iff some PDA recognizes it. The forward direction is the CFG → PDA construction; the reverse is the PDA → CFG construction.