Let b be given.

An exact proof term for the current goal is (famunionE rational_numbers (λq1 : set ⇒ {halfopen_interval_left q1 q2|q2 ∈ rational_numbers}) b HbB).

Apply Hexq1 to the current goal.

Let q1 be given.

Assume Hq1pair.

Apply Hq1pair to the current goal.

Assume Hq1Q: q1 ∈ rational_numbers.

We prove the intermediate claim Hexq2: ∃q2 ∈ rational_numbers, b = halfopen_interval_left q1 q2.

An exact proof term for the current goal is (ReplE rational_numbers (λq2 : set ⇒ halfopen_interval_left q1 q2) b HbFam).

Apply Hexq2 to the current goal.

Let q2 be given.

Assume Hq2pair.

We prove the intermediate claim Hq2Q: q2 ∈ rational_numbers.

An exact proof term for the current goal is (andEL (q2 ∈ rational_numbers) (b = halfopen_interval_left q1 q2) Hq2pair).

We prove the intermediate claim Hbeq: b = halfopen_interval_left q1 q2.

An exact proof term for the current goal is (andER (q2 ∈ rational_numbers) (b = halfopen_interval_left q1 q2) Hq2pair).

rewrite the current goal using Hbeq (from left to right).

We prove the intermediate claim Hq1R: q1 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).

We prove the intermediate claim Hq2R: q2 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).

We prove the intermediate claim HbInLowerBasis: halfopen_interval_left q1 q2 ∈ R_lower_limit_basis.

We prove the intermediate claim HbFamR: halfopen_interval_left q1 q2 ∈ {halfopen_interval_left q1 bb|bb ∈ R}.

An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left q1 bb) q2 Hq2R).

An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) q1 (halfopen_interval_left q1 q2) Hq1R HbFamR).

An exact proof term for the current goal is HbInGen.