Let x0 of type ι be given.

Apply H0 with ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field1b x0 x1 x2 ∈ field0 x0.

Apply RealsStruct_eta with x0, λ x1 x2 . struct_b_b_r_e_e x2 ⟶ unpack_b_b_r_e_e_o x0 (λ x3 . λ x4 x5 : ι → ι → ι . λ x6 : ι → ι → ο . λ x7 x8 . explicit_Reals x3 x7 x8 x4 x5 x6) ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field1b x0 x3 x4 ∈ field0 x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: struct_b_b_r_e_e (pack_b_b_r_e_e (field0 x0) (field1b x0) (field2b x0) (RealsStruct_leq x0) (field4 x0) (RealsStruct_one x0)).

Assume H2: unpack_b_b_r_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 : ι → ι → ο . λ x5 x6 . explicit_Reals x1 x5 x6 x2 x3 x4).

Apply pack_struct_b_b_r_e_e_E1 with field0 x0, field1b x0, field2b x0, RealsStruct_leq x0, field4 x0, RealsStruct_one x0.

The subproof is completed by applying H1.

■

Proofgold Proof