Let f and g be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Set A to be the term Romega_clipped_diffs f g.
Set P to be the term (λr : set ⇒ R_lub A r).
We prove the intermediate claim HAinR: ∀a : set, a ∈ A → a ∈ R.
An exact proof term for the current goal is (Romega_clipped_diffs_in_R f g Hf Hg).
We prove the intermediate claim Hub: ∃u : set, u ∈ R ∧ ∀a : set, a ∈ A → a ∈ R → Rle a u.
An exact proof term for the current goal is (Romega_clipped_diffs_bounded f g Hf Hg).
We prove the intermediate claim HAnen: ∃a0 : set, a0 ∈ A.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We use (Romega_coord_clipped_diff f g 0) to witness the existential quantifier.
An exact proof term for the current goal is (ReplI ω (λn : set ⇒ Romega_coord_clipped_diff f g n) 0 H0omega).
We prove the intermediate claim Hex: ∃l : set, P l.
An exact proof term for the current goal is (R_lub_exists A HAnen HAinR Hub).
An exact proof term for the current goal is (Eps_i_ex P Hex).
∎