∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . In x2 x1 ⟶ x0 x2) ⟶ x0 0 ⟶ (∀ x1 . x0 x1 ⟶ x0 (Union x1)) ⟶ (∀ x1 . x0 x1 ⟶ x0 (Power x1)) ⟶ (∀ x1 . x0 x1 ⟶ ∀ x2 : ι → ι . (∀ x3 . In x3 x1 ⟶ x0 (x2 x3)) ⟶ x0 (Repl x1 x2)) ⟶ ∀ x1 . x0 x1 |
|