Proofgold Address

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known In_ind : ∀ x0 : ι → ο . (∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . x0 x1
Theorem In_irref : ∀ x0 . nIn x0 x0 (proof)
Theorem 3dfc6.. : ∀ x0 x1 x2 . prim1 x0 x1 ⟶ prim1 x1 x2 ⟶ nIn x2 x0 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known Eps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (prim0 x0)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem Eps_i_set_R : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ and (prim1 (prim0 (λ x3 . and (prim1 x3 x0) (x1 x3))) x0) (x1 (prim0 (λ x3 . and (prim1 x3 x0) (x1 x3)))) (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition If_i := λ x0 : ο . λ x1 x2 . prim0 (λ x3 . or (and x0 (x3 = x1)) (and (not x0) (x3 = x2)))
Known xm : ∀ x0 : ο . or x0 (not x0)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem If_i_correct : ∀ x0 : ο . ∀ x1 x2 . or (and x0 (If_i x0 x1 x2 = x1)) (and (not x0) (If_i x0 x1 x2 = x2)) (proof)
Known andEL : ∀ x0 x1 : ο . and x0 x1 ⟶ x0
Known andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Theorem If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2 (proof)
Theorem If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1 (proof)
Theorem If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2) (proof)
Theorem If_i_eta : ∀ x0 : ο . ∀ x1 . If_i x0 x1 x1 = x1 (proof)
Theorem 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 : ∀ x0 x1 : (ι → ι → ι) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ι . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ι . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem 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 : ∀ x0 x1 : (ι → ι → ο) → ο . (∀ x2 : ο . (∀ x3 : ι → ι → ο . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 : ι → ι → ο . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2 (proof)
Theorem 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 := λ x0 : (ι → ι) → ο . λ x1 . prim0 (λ x2 . ∀ x3 : ι → ι . x0 x3 ⟶ x3 x1 = x2)
Theorem 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 := λ x0 : (ι → ι → ι) → ο . λ x1 x2 . prim0 (λ x3 . ∀ x4 : ι → ι → ι . x0 x4 ⟶ x4 x1 x2 = x3)
Theorem 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 := λ x0 : (ι → ι → ο) → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . x0 x3 ⟶ x3 x1 x2
Known prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Theorem 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 := λ x0 : (ι → ο) → ο . λ x1 . ∀ x2 : ι → ο . x0 x2 ⟶ x2 x1
Theorem 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 := λ x0 : ((ι → ο) → ο) → ο . λ x1 : ι → ο . ∀ x2 : (ι → ο) → ο . x0 x2 ⟶ x2 x1
Theorem 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 := λ x0 : ο . λ x1 x2 : ι → ι . λ x3 . If_i x0 (x1 x3) (x2 x3)
Theorem If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0 ⟶ If_ii x0 x1 x2 = x1 (proof)
Theorem If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0 ⟶ If_ii x0 x1 x2 = x2 (proof)
Definition If_iii := λ x0 : ο . λ x1 x2 : ι → ι → ι . λ x3 x4 . If_i x0 (x1 x3 x4) (x2 x3 x4)
Theorem If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0 ⟶ If_iii x0 x1 x2 = x1 (proof)
Theorem If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0 ⟶ If_iii x0 x1 x2 = x2 (proof)
Definition If_Vo1 := λ x0 : ο . λ x1 x2 : ι → ο . λ x3 . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem If_Vo1_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . x0 ⟶ If_Vo1 x0 x1 x2 = x1 (proof)
Theorem If_Vo1_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ο . not x0 ⟶ If_Vo1 x0 x1 x2 = x2 (proof)
Definition If_iio := λ x0 : ο . λ x1 x2 : ι → ι → ο . λ x3 x4 . and (x0 ⟶ x1 x3 x4) (not x0 ⟶ x2 x3 x4)
Theorem If_iio_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . x0 ⟶ If_iio x0 x1 x2 = x1 (proof)
Theorem If_iio_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ο . not x0 ⟶ If_iio x0 x1 x2 = x2 (proof)
Definition If_Vo2 := λ x0 : ο . λ x1 x2 : (ι → ο) → ο . λ x3 : ι → ο . and (x0 ⟶ x1 x3) (not x0 ⟶ x2 x3)
Theorem If_Vo2_1 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . x0 ⟶ If_Vo2 x0 x1 x2 = x1 (proof)
Theorem If_Vo2_0 : ∀ x0 : ο . ∀ x1 x2 : (ι → ο) → ο . not x0 ⟶ If_Vo2 x0 x1 x2 = x2 (proof)
Definition In_rec_i_G := λ x0 : ι → (ι → ι) → ι . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 . ∀ x5 : ι → ι . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_i := λ x0 : ι → (ι → ι) → ι . λ x1 . prim0 (In_rec_i_G x0 x1)
Theorem In_rec_i_G_c : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 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 : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 x2 . In_rec_i_G x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι . and (∀ x5 . prim1 x5 x1 ⟶ In_rec_i_G x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_i_G_f : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . ∀ x2 x3 : ι → ι . (∀ x4 . prim1 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 := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . λ x2 : ι → ι . ∀ x3 : ι → (ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_ii := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . Descr_ii (In_rec_G_ii x0 x1)
Theorem In_rec_G_ii_c : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 . prim1 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 : ∀ x0 : ι → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 : ι → ι . In_rec_G_ii x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι . and (∀ x5 . prim1 x5 x1 ⟶ In_rec_G_ii x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_G_ii_f : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 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 := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . λ x2 : ι → ι → ι . ∀ x3 : ι → (ι → ι → ι) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ι . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_iii := λ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . λ x1 . Descr_iii (In_rec_G_iii x0 x1)
Theorem In_rec_G_iii_c : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι → ι . (∀ x3 . prim1 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 : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι . In_rec_G_iii x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ι . and (∀ x5 . prim1 x5 x1 ⟶ In_rec_G_iii x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem In_rec_G_iii_f : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 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 : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 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 94aee.. := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . λ x2 : ι → ι → ο . ∀ x3 : ι → (ι → ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ι → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_iio := λ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . λ x1 . Descr_iio (94aee.. x0 x1)
Theorem bc67e.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ι → ο . (∀ x3 . prim1 x3 x1 ⟶ 94aee.. x0 x3 (x2 x3)) ⟶ 94aee.. x0 x1 (x0 x1 x2) (proof)
Theorem 9f718.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . 94aee.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ι → ο . and (∀ x5 . prim1 x5 x1 ⟶ 94aee.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 0bcfd.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ι → ο . 94aee.. x0 x1 x2 ⟶ 94aee.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 39b30.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 94aee.. x0 x1 (In_rec_iio x0 x1) (proof)
Theorem a4174.. : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 94aee.. x0 x1 (x0 x1 (In_rec_iio x0)) (proof)
Theorem In_rec_iio_eq : ∀ x0 : ι → (ι → ι → ι → ο) → ι → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ο . (∀ x4 . prim1 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 1d55d.. := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . λ x2 : ι → ο . ∀ x3 : ι → (ι → ο) → ο . (∀ x4 . ∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo1 := λ x0 : ι → (ι → ι → ο) → ι → ο . λ x1 . Descr_Vo1 (1d55d.. x0 x1)
Theorem 8b22b.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 . prim1 x3 x1 ⟶ 1d55d.. x0 x3 (x2 x3)) ⟶ 1d55d.. x0 x1 (x0 x1 x2) (proof)
Theorem 946ce.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ο . 1d55d.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ι → ο . and (∀ x5 . prim1 x5 x1 ⟶ 1d55d.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem 27d99.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : ι → ο . 1d55d.. x0 x1 x2 ⟶ 1d55d.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem dd8c7.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 1d55d.. x0 x1 (In_rec_Vo1 x0 x1) (proof)
Theorem 24637.. : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 1d55d.. x0 x1 (x0 x1 (In_rec_Vo1 x0)) (proof)
Theorem In_rec_Vo1_eq : ∀ x0 : ι → (ι → ι → ο) → ι → ο . (∀ x1 . ∀ x2 x3 : ι → ι → ο . (∀ x4 . prim1 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 cdf76.. := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . λ x2 : (ι → ο) → ο . ∀ x3 : ι → ((ι → ο) → ο) → ο . (∀ x4 . ∀ x5 : ι → (ι → ο) → ο . (∀ x6 . prim1 x6 x4 ⟶ x3 x6 (x5 x6)) ⟶ x3 x4 (x0 x4 x5)) ⟶ x3 x1 x2
Definition In_rec_Vo2 := λ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . λ x1 . Descr_Vo2 (cdf76.. x0 x1)
Theorem c0fdc.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → (ι → ο) → ο . (∀ x3 . prim1 x3 x1 ⟶ cdf76.. x0 x3 (x2 x3)) ⟶ cdf76.. x0 x1 (x0 x1 x2) (proof)
Theorem 7f73e.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . cdf76.. x0 x1 x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → (ι → ο) → ο . and (∀ x5 . prim1 x5 x1 ⟶ cdf76.. x0 x5 (x4 x5)) (x2 = x0 x1 x4) ⟶ x3) ⟶ x3 (proof)
Theorem ddf85.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . ∀ x2 x3 : (ι → ο) → ο . cdf76.. x0 x1 x2 ⟶ cdf76.. x0 x1 x3 ⟶ x2 = x3 (proof)
Theorem 4604c.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . cdf76.. x0 x1 (In_rec_Vo2 x0 x1) (proof)
Theorem a7ca6.. : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . cdf76.. x0 x1 (x0 x1 (In_rec_Vo2 x0)) (proof)
Theorem In_rec_Vo2_eq : ∀ x0 : ι → (ι → (ι → ο) → ο) → (ι → ο) → ο . (∀ x1 . ∀ x2 x3 : ι → (ι → ο) → ο . (∀ x4 . prim1 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)