Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply set_ext with RealsStruct_Q x0, {x1 ∈ field0 x0|∃ x2 . and (x2 ∈ {x3 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x3 ∈ RealsStruct_Npos x0) (x3 = field4 x0)) (x3 ∈ RealsStruct_Npos x0)}) (∃ x3 . and (x3 ∈ RealsStruct_Npos x0) (field2b x0 x3 x1 = x2))} leaving 2 subgoals.

Let x1 of type ι be given.

Assume H1: x1 ∈ RealsStruct_Q x0.

Apply SepE with field0 x0, 2a63f.. x0, x1, x1 ∈ {x2 ∈ field0 x0|∃ x3 . and (x3 ∈ {x4 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x4 ∈ RealsStruct_Npos x0) (x4 = field4 x0)) (x4 ∈ RealsStruct_Npos x0)}) (∃ x4 . and (x4 ∈ RealsStruct_Npos x0) (field2b x0 x4 x2 = x3))} leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H2: x1 ∈ field0 x0.

Assume H3: 2a63f.. x0 x1.

Apply SepI with field0 x0, λ x2 . ∃ x3 . and (x3 ∈ {x4 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x4 ∈ RealsStruct_Npos x0) (x4 = field4 x0)) (x4 ∈ RealsStruct_Npos x0)}) (∃ x4 . and (x4 ∈ RealsStruct_Npos x0) (field2b x0 x4 x2 = x3)), x1 leaving 2 subgoals.

The subproof is completed by applying H2.

Apply unknownprop_87925c67a03b35d7e2b95672013636ce0205b3bb767f5d1c0c78f69cadaeb3e9 with x0, λ x2 x3 . ∃ x4 . and (x4 ∈ x2) (∃ x5 . and (x5 ∈ RealsStruct_Npos x0) (field2b x0 x5 x1 = x4)) leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

Let x1 of type ι be given.

Assume H1: x1 ∈ {x2 ∈ field0 x0|∃ x3 . and (x3 ∈ {x4 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x4 ∈ RealsStruct_Npos x0) (x4 = field4 x0)) (x4 ∈ RealsStruct_Npos x0)}) (∃ x4 . and (x4 ∈ RealsStruct_Npos x0) (field2b x0 x4 x2 = x3))}.

Apply SepE with field0 x0, λ x2 . ∃ x3 . and (x3 ∈ {x4 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x4 ∈ RealsStruct_Npos x0) (x4 = field4 x0)) (x4 ∈ RealsStruct_Npos x0)}) (∃ x4 . and ... ...), ..., ... leaving 2 subgoals.

...

■

Proofgold Proof