Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Claim L1: ...

...

Apply functional extensionality with λ x1 x2 . ap (ap (ap (Field_of_RealsStruct x0) 1) x1) x2, field1b x0.

Let x1 of type ι be given.

Apply functional extensionality with (λ x2 x3 . ap (ap (ap (Field_of_RealsStruct x0) 1) x2) x3) x1, field1b x0 x1.

Let x2 of type ι be given.

set y3 to be ...

set y4 to be ...

Claim L2: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3

Let x5 of type ι → ο be given.

Assume H2: x5 (field1b x2 y3 y4).

set y6 to be ...

set y7 to be ...

Claim L3: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6

Let x8 of type ι → ο be given.

Assume H3: x8 (ap (ap (encode_b (field0 y4) (field1b y4)) x5) y6).

set y9 to be ...

set y10 to be ap (ap (lam 5 (λ x10 . If_i (x10 = 0) (field0 y4) (If_i (x10 = 1) (encode_b (field0 y4) (field1b y4)) (If_i (x10 = 2) (encode_b (field0 y4) (field2b y4)) (If_i (x10 = 3) ... ...))))) 1) ...

set y11 to be ap (encode_b (field0 x5) (field1b x5)) y6

Claim L4: ∀ x12 : ι → ο . x12 y11 ⟶ x12 y10

Let x12 of type ι → ο be given.

Assume H4: x12 (ap (encode_b (field0 y6) (field1b y6)) y7).

set y13 to be λ x13 . x12

Apply tuple_5_1_eq with field0 y6, encode_b (field0 y6) (field1b y6), encode_b (field0 y6) (field2b y6), field4 y6, RealsStruct_one y6, λ x14 x15 . y13 (ap x14 y7) (ap x15 y7).

The subproof is completed by applying H4.

set y12 to be λ x12 x13 . y11 (ap x12 x8) (ap x13 x8)

Apply L4 with λ x13 . y12 x13 y11 ⟶ y12 y11 x13 leaving 2 subgoals.

Assume H5: y12 y11 y11.

The subproof is completed by applying H5.

The subproof is completed by applying L4.

set y8 to be λ x8 . y7

Apply L3 with λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.

Assume H4: y8 y7 y7.

The subproof is completed by applying H4.

Apply RealsStruct_eta with x5, λ x9 x10 . ap (ap (encode_b (field0 x5) (field1b x5)) y6) y7 = field1b x10 y6 y7, λ x9 . y8 leaving 3 subgoals.

The subproof is completed by applying L1.

Apply tuple_6_1_eq with field0 x5, encode_b (field0 x5) (field1b x5), encode_b (field0 x5) (field2b x5), encode_r (field0 x5) (RealsStruct_leq x5), field4 x5, RealsStruct_one x5, λ x9 x10 . ap (ap (encode_b (field0 x5) (field1b x5)) y6) y7 = decode_b x10 y6 y7.

Let x9 of type ι → ι → ο be given.

Assume H4: x9 (ap (ap (encode_b (field0 x5) (field1b x5)) y6) y7) (decode_b (encode_b (field0 x5) (field1b x5)) y6 y7).

The subproof is completed by applying H4.

The subproof is completed by applying L3.

Let x5 of type ι → ι → ο be given.

Apply L2 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.

Assume H3: x5 y4 y4.

The subproof is completed by applying H3.

■

Proofgold Proof