Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known In_ind^In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . x2 ∈ x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem 258d1.. : ∀ x0 x1 x2 . x0 ∈ x1 ⟶ x1 ∈ x2 ⟶ nIn x2 x0 (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known Eps_i_ax^Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem Eps_i_set_R^Eps_i_set_R : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ and (prim0 (λ x3 . and (x3 ∈ x0) (x1 x3)) ∈ x0) (x1 (prim0 (λ x3 . and (x3 ∈ x0) (x1 x3)))) (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition If_i^If_i := λ x0 : ο . λ x1 x2 . prim0 (λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)))
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known If_i_correct^If_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2))
Known andEL^andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known andER^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known If_i_or^If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Known If_i_eta^If_i_eta : ∀ x0 : ο . ∀ x1 . If_i x0 x1 x1 = x1
Theorem exandE_ii^exandE_ii : ∀ x0 x1 : (ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iii^exandE_iii : ∀ x0 x1 : (ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iiii^exandE_iiii : ∀ x0 x1 : (ι → ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iio^exandE_iio : ∀ x0 x1 : (ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ο . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem exandE_iiio^exandE_iiio : ∀ x0 x1 : (ι → ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Definition Descr_ii^Descr_ii := λ x0 : (ι → ι) → ο . λ x1 . prim0 (λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x1 = x2)
Theorem Descr_ii_prop^{Descr_ii_prop} : ∀ x0 : (ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_ii x0) (proof)
Definition Descr_iii^Descr_iii := λ x0 : (ι → ι → ι) → ο . λ x1 x2 . prim0 (λ x3 . ∀ x4 : ι → ι → ι . x0 x4 ⟶ x4 x1 x2 = x3)
Theorem Descr_iii_prop^{Descr_iii_prop} : ∀ x0 : (ι → ι → ι) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ι . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι → ι . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iii x0) (proof)
Definition Descr_iio^Descr_iio := λ x0 : (ι → ι → ο) → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . x0 x3 ⟶ x3 x1 x2
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem Descr_iio_prop^{Descr_iio_prop} : ∀ x0 : (ι → ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_iio x0) (proof)
Definition Descr_Vo1^Descr_Vo1 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo1_prop^{Descr_Vo1_prop} : ∀ x0 : (ι → ο) → ο . (∀ x1 : ο . (∀ x2 : ι → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : ι → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo1 x0) (proof)
Definition Descr_Vo2^Descr_Vo2 := λ x0 : ((ι → ο) → ο) → ο . λ x1 : ι → ο . ∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x2 x1
Theorem Descr_Vo2_prop^{Descr_Vo2_prop} : ∀ x0 : ((ι → ο) → ο) → ο . (∀ x1 : ο . (∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x1) ⟶ x1) ⟶ (∀ x1 x2 : (ι → ο) → ο . x0 x1 ⟶ x0 x2 ⟶ x1 = x2) ⟶ x0 (Descr_Vo2 x0) (proof)
Definition If_ii^If_ii := λ x0 : ο . λ x1 x2 : ι → ι . λ x3 . If_i x0 (x1 x3) (x2 x3)
Theorem If_ii_1^If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0 ⟶ If_ii x0 x1 x2 = x1 (proof)
Theorem If_ii_0^If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0 ⟶ If_ii x0 x1 x2 = x2 (proof)
Definition If_iii^If_iii := λ x0 : ο . λ x1 x2 : ι → ι → ι . λ x3 x4 . If_i x0 (x1 x3 x4) (x2 x3 x4)
Theorem If_iii_1^If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0 ⟶ If_iii x0 x1 x2 = x1 (proof)
Theorem If_iii_0^If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0 ⟶ If_iii x0 x1 x2 = x2 (proof)
Definition If_Vo1^If_Vo1 := λ x0 : ο . λ x1 x2 : ι → ο . λ x3 . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem If_Vo1_1^If_Vo1_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . x0 ⟶ If_Vo1 x0 x1 x2 = x1 (proof)
Theorem If_Vo1_0^If_Vo1_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . not x0 ⟶ If_Vo1 x0 x1 x2 = x2 (proof)
Definition If_iio^If_iio := λ x0 : ο . λ x1 x2 : ι → ι → ο . λ x3 x4 . and (x0 ⟶ x1 x3 x4) (not x0 ⟶ x2 x3 x4)
Theorem If_iio_1^If_iio_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . x0 ⟶ If_iio x0 x1 x2 = x1 (proof)
Theorem If_iio_0^If_iio_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . not x0 ⟶ If_iio x0 x1 x2 = x2 (proof)
Definition If_Vo2^If_Vo2 := λ x0 : ο . λ x1 x2 : (ι → ο) → ο . λ x3 : ι → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Theorem If_Vo2_1^If_Vo2_1 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . x0 ⟶ If_Vo2 x0 x1 x2 = x1 (proof)
Theorem If_Vo2_0^If_Vo2_0 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . not x0 ⟶ If_Vo2 x0 x1 x2 = x2 (proof)
Definition In_rec_i_G^In_rec_i_G := λ x0 : ι → (ι → ι) → ι . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 . ∀ x5 : ι → ι . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_i^In_rec_i := λ x0 : ι → (ι → ι) → ι . λ x1 . prim0 (In_rec_i_G x0 x1)
Theorem In_rec_i_G_c^In_rec_i_G_c : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ In_rec_i_G x0 x3 (x2 x3)) ⟶ In_rec_i_G x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_i_G_inv^{In_rec_i_G_inv} : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 x2 . In_rec_i_G x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι . and (∀ x5 . x5 ∈ x1 ⟶ In_rec_i_G x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_i_G_f^In_rec_i_G_f : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 x2 x3 . In_rec_i_G x0 x1 x2 ⟶ In_rec_i_G x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem In_rec_i_G_In_rec_i^{In_rec_i_G_In_rec_i} : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i_G x0 x1 (In_rec_i x0 x1) (proof)
Theorem In_rec_i_G_In_rec_i_d^{In_rec_i_G_In_rec_i_d} : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i_G x0 x1 (x0 x1 (In_rec_i x0)) (proof)
Theorem In_rec_i_eq^In_rec_i_eq : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_i x0 x1 = x0 x1 (In_rec_i x0) (proof)
Definition In_rec_G_ii^In_rec_G_ii := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . λ x2 : ι → ι . ∀ x3 : ι → (ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_ii^In_rec_ii := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . Descr_ii (In_rec_G_ii x0 x1)
Theorem In_rec_G_ii_c^{In_rec_G_ii_c} : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x1 ⟶ In_rec_G_ii x0 x3 (x2 x3)) ⟶ In_rec_G_ii x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_G_ii_inv^{In_rec_G_ii_inv} : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . In_rec_G_ii x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι . and (∀ x5 . x5 ∈ x1 ⟶ In_rec_G_ii x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_G_ii_f^{In_rec_G_ii_f} : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι . In_rec_G_ii x0 x1 x2 ⟶ In_rec_G_ii x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem In_rec_G_ii_In_rec_ii^{In_rec_G_ii_In_rec_ii} : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_ii x0 x1 (In_rec_ii x0 x1) (proof)
Theorem In_rec_G_ii_In_rec_ii_d^{In_rec_G_ii_In_rec_ii_d} : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_ii x0 x1 (x0 x1 (In_rec_ii x0)) (proof)
Theorem In_rec_ii_eq^In_rec_ii_eq : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_ii x0 x1 = x0 x1 (In_rec_ii x0) (proof)
Definition In_rec_G_iii^In_rec_G_iii := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . λ x2 : ι → ι → ι . ∀ x3 : ι → (ι → ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ι . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_iii^In_rec_iii := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . Descr_iii (In_rec_G_iii x0 x1)
Theorem In_rec_G_iii_c^{In_rec_G_iii_c} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι → ι . (∀ x3 . x3 ∈ x1 ⟶ In_rec_G_iii x0 x3 (x2 x3)) ⟶ In_rec_G_iii x0 x1 (x0 x1 x2) (proof)
Theorem In_rec_G_iii_inv^{In_rec_G_iii_inv} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . In_rec_G_iii x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ι . and (∀ x5 . x5 ∈ x1 ⟶ In_rec_G_iii x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_G_iii_f^{In_rec_G_iii_f} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ι . In_rec_G_iii x0 x1 x2 ⟶ In_rec_G_iii x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem In_rec_G_iii_In_rec_iii^{In_rec_G_iii_In_rec_iii} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_iii x0 x1 (In_rec_iii x0 x1) (proof)
Theorem In_rec_G_iii_In_rec_iii_d^{In_rec_G_iii_In_rec_iii_d} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_G_iii x0 x1 (x0 x1 (In_rec_iii x0)) (proof)
Theorem In_rec_iii_eq^{In_rec_iii_eq} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_iii x0 x1 = x0 x1 (In_rec_iii x0) (proof)
Definition 6b023.. := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . λ x2 : ι → ι → ο . ∀ x3 : ι → (ι → ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ο . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_iio^In_rec_iio := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . Descr_iio (6b023.. x0 x1)
Theorem 6f12d.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ 6b023.. x0 x3 (x2 x3)) ⟶ 6b023.. x0 x1 (x0 x1 x2) (proof)
Theorem b0c8e.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . 6b023.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ο . and (∀ x5 . x5 ∈ x1 ⟶ 6b023.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 41db9.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ο . 6b023.. x0 x1 x2 ⟶ 6b023.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 409d6.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6b023.. x0 x1 (In_rec_iio x0 x1) (proof)
Theorem 67223.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 6b023.. x0 x1 (x0 x1 (In_rec_iio x0)) (proof)
Theorem In_rec_iio_eq^{In_rec_iio_eq} : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_iio x0 x1 = x0 x1 (In_rec_iio x0) (proof)
Definition f6068.. := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ι → (ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ο . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo1^In_rec_Vo1 := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . Descr_Vo1 (f6068.. x0 x1)
Theorem 0d2cd.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ f6068.. x0 x3 (x2 x3)) ⟶ f6068.. x0 x1 (x0 x1 x2) (proof)
Theorem 4d242.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ο . f6068.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x1 ⟶ f6068.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem ebaf1.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ο . f6068.. x0 x1 x2 ⟶ f6068.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 2f624.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . f6068.. x0 x1 (In_rec_Vo1 x0 x1) (proof)
Theorem 722ac.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . f6068.. x0 x1 (x0 x1 (In_rec_Vo1 x0)) (proof)
Theorem In_rec_Vo1_eq^{In_rec_Vo1_eq} : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_Vo1 x0 x1 = x0 x1 (In_rec_Vo1 x0) (proof)
Definition 2b1c2.. := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . λ x2 : (ι → ο) → ο . ∀ x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (ι → ο) → ο . (∀ x6 . x6 ∈ x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo2^In_rec_Vo2 := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . Descr_Vo2 (2b1c2.. x0 x1)
Theorem 07e5d.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → (ι → ο) → ο . (∀ x3 . x3 ∈ x1 ⟶ 2b1c2.. x0 x3 (x2 x3)) ⟶ 2b1c2.. x0 x1 (x0 x1 x2) (proof)
Theorem 994ef.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . 2b1c2.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → (ι → ο) → ο . and (∀ x5 . x5 ∈ x1 ⟶ 2b1c2.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem d8d0b.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (ι → ο) → ο . 2b1c2.. x0 x1 x2 ⟶ 2b1c2.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 2cb7a.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 2b1c2.. x0 x1 (In_rec_Vo2 x0 x1) (proof)
Theorem 00e25.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 2b1c2.. x0 x1 (x0 x1 (In_rec_Vo2 x0)) (proof)
Theorem In_rec_Vo2_eq^{In_rec_Vo2_eq} : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_Vo2 x0 x1 = x0 x1 (In_rec_Vo2 x0) (proof)