Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι → ι → ι be given.

Let x4 of type ι → ι → ι be given.

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

Let x6 of type ο be given.

Assume H0: 62ee1.. x0 x1 x2 x3 x4 x5 ⟶ explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ lt x0 x1 x2 x3 x4 x5 x1 x7 ⟶ x5 x1 x8 ⟶ ∃ x9 . and (prim1 x9 (1216a.. x0 (λ x10 . natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10))) (x5 x8 (x4 x9 x7))) ⟶ (∀ x7 . prim1 x7 (b5c9f.. x0 (1216a.. x0 (λ x8 . natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8))) ⟶ ∀ x8 . prim1 x8 (b5c9f.. x0 (1216a.. x0 (λ x9 . natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9))) ⟶ (∀ x9 . prim1 x9 (1216a.. x0 (λ x10 . natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10)) ⟶ and (and (x5 (f482f.. x7 x9) (f482f.. x8 x9)) (x5 (f482f.. x7 x9) (f482f.. x7 (x3 x9 x2)))) (x5 (f482f.. x8 (x3 x9 x2)) (f482f.. x8 x9))) ⟶ ∃ x9 . and (prim1 x9 x0) (∀ x10 . prim1 x10 (1216a.. x0 (λ x11 . natOfOrderedField_p x0 x1 x2 x3 x4 x5 x11)) ⟶ and (x5 (f482f.. x7 x10) x9) (x5 x9 (f482f.. x8 x10)))) ⟶ x6.

Assume H1: 62ee1.. x0 x1 x2 x3 x4 x5.

Apply and3E with explicit_OrderedField x0 x1 x2 x3 x4 x5, ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ lt x0 x1 x2 x3 x4 x5 x1 x7 ⟶ x5 x1 x8 ⟶ ∃ x9 . and (prim1 x9 (1216a.. x0 (λ x10 . natOfOrderedField_p x0 x1 x2 x3 x4 x5 x10))) (x5 x8 (x4 x9 x7)), ∀ x7 . ... ⟶ ∀ x8 . ... ⟶ (∀ x9 . ... ⟶ and (and (x5 ... ...) ...) ...) ⟶ ∃ x9 . and (prim1 x9 x0) (∀ x10 . prim1 x10 (1216a.. x0 (λ x11 . natOfOrderedField_p x0 x1 x2 x3 x4 x5 x11)) ⟶ and (x5 (f482f.. x7 x10) x9) (x5 x9 (f482f.. x8 x10))), ... leaving 2 subgoals.

...

■

Proofgold Proof