We will prove rational_open_intervals_basis ⊆ R_standard_basis.
Let I be given.
Assume HI: I ∈ rational_open_intervals_basis.
Apply (famunionE_impred rational_numbers (λq1 : set ⇒ {open_interval q1 q2|q2 ∈ rational_numbers}) I HI (I ∈ R_standard_basis)) to the current goal.
Let q1 be given.
Assume Hq1Q HIq1.
Apply (ReplE_impred rational_numbers (λq2 : set ⇒ open_interval q1 q2) I HIq1 (I ∈ R_standard_basis)) to the current goal.
Let q2 be given.
Assume Hq2Q Heq.
rewrite the current goal using Heq (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 HIq2: open_interval q1 q2 ∈ {open_interval q1 b|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb : set ⇒ open_interval q1 b) q2 Hq2R).
An exact proof term for the current goal is (famunionI R (λa : set ⇒ {open_interval a b|b ∈ R}) q1 (open_interval q1 q2) Hq1R HIq2).
∎