We will prove infinite long_line.
We prove the intermediate claim Hex: ∃L : set, infinite L.
We use ω to witness the existential quantifier.
An exact proof term for the current goal is infinite_omega.
An exact proof term for the current goal is (Eps_i_ex (λL : set ⇒ infinite L) Hex).
∎