Proofgold Address

Param lam^Sigma : ι → (ι → ι) → ι
Definition setprod^setprod := λ x0 x1 . lam x0 (λ x2 . x1)
Param ap^ap : ι → ι → ι
Known ap0_Sigma^ap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 0 ∈ x0
Theorem 2c199.. : ∀ x0 x1 x2 . x2 ∈ setprod x0 x1 ⟶ ap x2 0 ∈ x0
Param ordsucc^ordsucc : ι → ι
Known ap1_Sigma^ap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ap x2 1 ∈ x1 (ap x2 0)
Theorem f9e57.. : ∀ x0 x1 x2 . x2 ∈ setprod x0 x1 ⟶ ap x2 1 ∈ x1
Param If_i^If_i : ο → ι → ι → ι
Known tuple_Sigma_eta^{tuple_Sigma_eta} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Theorem 442b3.. : ∀ x0 x1 x2 . x2 ∈ setprod x0 x1 ⟶ lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2