Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply Field_of_RealsStruct_1f with x0, λ x1 x2 : ι → ι → ι . ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ field0 x0 ⟶ x1 x3 x4 = x1 x3 x5 ⟶ x4 = x5 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply explicit_Field_plus_cancelL with field0 x0, ap (Field_of_RealsStruct x0) 3, ap (Field_of_RealsStruct x0) 4, decode_b (ap (Field_of_RealsStruct x0) 1), decode_b (ap (Field_of_RealsStruct x0) 2).

Apply explicit_Field_of_RealsStruct_2 with x0.

The subproof is completed by applying H0.

■

Proofgold Proof