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.
Assume H1:
∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x6 x7 x8 = x6 x9 x10 ⟶ and (x7 = x9) (x8 = x10).
Let x7 of type ο be given.
Assume H2:
... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ (∀ x8 . ... ⟶ ∀ x9 . ... ⟶ (λ x10 . prim0 (λ x11 . (λ x12 x13 : ο . ∀ x14 : ο . (x12 ⟶ x13 ⟶ x14) ⟶ x14) (prim1 x11 x0) (x10 = x6 ((λ x12 . prim0 (λ x13 . (λ x14 x15 : ο . ∀ x16 : ο . (x14 ⟶ x15 ⟶ x16) ⟶ x16) (prim1 x13 x0) (∃ x14 . and (prim1 x14 x0) (x12 = x6 x13 x14)))) x10) x11))) ((λ x10 x11 . x6 (x3 (x4 ((λ x12 . prim0 (λ x13 . (λ x14 x15 : ο . ∀ x16 : ο . (x14 ⟶ x15 ⟶ x16) ⟶ x16) (prim1 x13 x0) (∃ x14 . and (prim1 x14 x0) (x12 = x6 x13 x14)))) x10) ((λ x12 . prim0 (λ x13 . (λ x14 x15 : ο . ∀ x16 : ο . (x14 ⟶ x15 ⟶ x16) ⟶ x16) (prim1 x13 x0) (∃ x14 . and (prim1 x14 x0) (x12 = x6 x13 x14)))) x11)) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 ((λ x12 . prim0 (λ x13 . (λ x14 x15 : ο . ∀ x16 : ο . (x14 ⟶ x15 ⟶ x16) ⟶ x16) (prim1 x13 x0) (x12 = x6 ((λ x14 . prim0 (λ x15 . (λ x16 x17 : ο . ∀ x18 : ο . (x16 ⟶ x17 ⟶ x18) ⟶ x18) (prim1 x15 x0) (∃ x16 . and (prim1 x16 x0) (x14 = x6 x15 x16)))) x12) x13))) x10) ((λ x12 . prim0 (λ x13 . (λ x14 x15 : ο . ∀ x16 : ο . (x14 ⟶ x15 ⟶ x16) ⟶ x16) (prim1 x13 x0) (x12 = x6 ((λ x14 . prim0 (λ x15 . (λ x16 x17 : ο . ∀ x18 : ο . (x16 ⟶ x17 ⟶ x18) ⟶ x18) (prim1 x15 x0) (∃ x16 . and (prim1 x16 x0) (x14 = x6 x15 x16)))) x12) x13))) x11)))) (x3 (x4 ((λ x12 . prim0 (λ x13 . (λ x14 x15 : ο . ∀ x16 : ο . (x14 ⟶ x15 ⟶ x16) ⟶ x16) (prim1 x13 x0) (∃ x14 . and (prim1 x14 x0) (x12 = x6 x13 x14)))) x10) ((λ x12 . prim0 (λ x13 . (λ x14 x15 : ο . ∀ x16 : ο . (x14 ⟶ x15 ⟶ x16) ⟶ x16) (prim1 x13 x0) ...)) ...)) ...)) ... ...) = ...) ⟶ x7.