Proofgold Address

Param lam^Sigma : ι → (ι → ι) → ι
Param ordsucc^ordsucc : ι → ι
Param ap^ap : ι → ι → ι
Param If_i^If_i : ο → ι → ι → ι
Known lam_eta^lam_eta : ∀ x0 . ∀ x1 : ι → ι . lam x0 (ap (lam x0 x1)) = lam x0 x1
Theorem tuple_3_eta^tuple_3_eta : ∀ x0 x1 x2 . lam 3 (ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2)))) = lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2)) (proof)
Theorem tuple_4_eta^tuple_4_eta : ∀ x0 x1 x2 x3 . lam 4 (ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))))) = lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))) (proof)
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known In_0_3^In_0_3 : 0 ∈ 3
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem tuple_3_0_eq^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0 (proof)
Known In_1_3^In_1_3 : 1 ∈ 3
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known neq_1_0^neq_1_0 : 1 = 0 ⟶ ∀ x0 : ο . x0
Theorem tuple_3_1_eq^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1 (proof)
Known In_2_3^In_2_3 : 2 ∈ 3
Known neq_2_0^neq_2_0 : 2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : 2 = 1 ⟶ ∀ x0 : ο . x0
Theorem tuple_3_2_eq^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2 (proof)
Known In_0_4^In_0_4 : 0 ∈ 4
Theorem tuple_4_0_eq^tuple_4_0_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 0 = x0 (proof)
Known In_1_4^In_1_4 : 1 ∈ 4
Theorem tuple_4_1_eq^tuple_4_1_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 1 = x1 (proof)
Known In_2_4^In_2_4 : 2 ∈ 4
Theorem tuple_4_2_eq^tuple_4_2_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 2 = x2 (proof)
Known In_3_4^In_3_4 : 3 ∈ 4
Known neq_3_0^neq_3_0 : 3 = 0 ⟶ ∀ x0 : ο . x0
Known neq_3_1^neq_3_1 : 3 = 1 ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : 3 = 2 ⟶ ∀ x0 : ο . x0
Theorem tuple_4_3_eq^tuple_4_3_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 3 = x3 (proof)
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known cases_3^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Theorem tuple_3_in_A_3^{tuple_3_in_A_3} : ∀ x0 x1 x2 x3 . x0 ∈ x3 ⟶ x1 ∈ x3 ⟶ x2 ∈ x3 ⟶ lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2)) ∈ setexp x3 3 (proof)
Param bij^bij : ι → ι → (ι → ι) → ο
Param nat_p^nat_p : ι → ο
Known PigeonHole_nat_bij^{PigeonHole_nat_bij} : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ x0) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known nat_2^nat_2 : nat_p 2
Theorem tuple_3_bij_3^{tuple_3_bij_3} : ∀ x0 x1 x2 . x0 ∈ 3 ⟶ x1 ∈ 3 ⟶ x2 ∈ 3 ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ bij 3 3 (ap (lam 3 (λ x3 . If_i (x3 = 0) x0 (If_i (x3 = 1) x1 x2)))) (proof)
Known cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Theorem tuple_4_in_A_4^{tuple_4_in_A_4} : ∀ x0 x1 x2 x3 x4 . x0 ∈ x4 ⟶ x1 ∈ x4 ⟶ x2 ∈ x4 ⟶ x3 ∈ x4 ⟶ lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))) ∈ setexp x4 4 (proof)
Theorem tuple_4_bij_4^{tuple_4_bij_4} : ∀ x0 x1 x2 x3 . x0 ∈ 4 ⟶ x1 ∈ 4 ⟶ x2 ∈ 4 ⟶ x3 ∈ 4 ⟶ (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ bij 4 4 (ap (lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 (If_i (x4 = 2) x2 x3))))) (proof)