| λ x0 . λ x1 x2 : ι → ι . λ x3 x4 x5 . λ x6 x7 : ι → ι → ι . and (and (and (and (and (and (and (and (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) |
|