| ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 x5 . ∀ x6 x7 : ι → ι → ι . explicit_Field x0 x3 x4 x6 x7 ⟶ (∀ x8 : ο . (∀ x9 : ι → ι → ο . 62ee1.. (1216a.. x0 (λ x10 . x1 x10 = x10)) x3 x4 x6 x7 x9 ⟶ x8) ⟶ x8) ⟶ (∀ x8 . prim1 x8 x0 ⟶ prim1 (x2 x8) (1216a.. x0 (λ x9 . x1 x9 = x9))) ⟶ prim1 x5 x0 ⟶ (∀ x8 . prim1 x8 x0 ⟶ prim1 (x1 x8) x0) ⟶ (∀ x8 . prim1 x8 x0 ⟶ prim1 (x2 x8) x0) ⟶ (∀ x8 . prim1 x8 x0 ⟶ x8 = x6 (x1 x8) (x7 x5 (x2 x8))) ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x1 x8 = x1 x9 ⟶ x2 x8 = x2 x9 ⟶ x8 = x9) ⟶ x6 (x7 x5 x5) x4 = x3 ⟶ 11fac.. x0 x1 x2 x3 x4 x5 x6 x7 |
|