Proofgold Asset

Definition ChurchBoolTru := λ x0 x1 . x0
Definition ChurchBoolFal := λ x0 x1 . x1
Theorem 6d4d5.. : ChurchBoolTru = λ x1 x2 . x1 (proof)
Theorem 87844.. : ChurchBoolFal = λ x1 x2 . x2 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition fb516.. := λ x0 : ι → ι → ι . or (x0 = ChurchBoolTru) (x0 = ChurchBoolFal)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem c8b93.. : fb516.. ChurchBoolTru (proof)
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem cff48.. : fb516.. ChurchBoolFal (proof)
Definition 6fb7f.. := λ x0 : ι → ι → ι . x0 = ChurchBoolFal
Definition permargs_i_1_0 := λ x0 : ι → ι → ι . λ x1 x2 . x0 x2 x1
Definition cc64c.. := λ x0 x1 : ι → ι → ι . λ x2 x3 . x0 x2 (x1 x2 x3)
Definition c2beb.. := λ x0 x1 : ι → ι → ι . λ x2 x3 . x0 (x1 x2 x3) x3
Definition efcd0.. := λ x0 x1 : ι → ι → ι . λ x2 x3 . x0 x3 (x1 x2 x3)
Definition 355fd.. := λ x0 x1 : ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2) (x1 x2 x3)
Param ordsucc^ordsucc : ι → ι
Known neq_0_1^neq_0_1 : 0 = 1 ⟶ ∀ x0 : ο . x0
Theorem e0d11.. : ChurchBoolTru = ChurchBoolFal ⟶ ∀ x0 : ο . x0 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 16271.. : not (6fb7f.. ChurchBoolTru) (proof)
Theorem 9e259.. : 6fb7f.. ChurchBoolFal (proof)
Param If_i^If_i : ο → ι → ι → ι
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
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
Theorem 2d3e7.. : ∀ x0 : ο . 6fb7f.. (λ x2 x3 . If_i x0 x3 x2) = x0 (proof)
Theorem 9e666.. : ∀ x0 : ι → ι → ι . 6fb7f.. (permargs_i_1_0 x0) ⟶ not (6fb7f.. x0) (proof)
Theorem 20d9c.. : permargs_i_1_0 ChurchBoolTru = ChurchBoolFal (proof)
Theorem 65f0e.. : permargs_i_1_0 ChurchBoolFal = ChurchBoolTru (proof)
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem ac767.. : ∀ x0 : ι → ι → ι . fb516.. x0 ⟶ 6fb7f.. (permargs_i_1_0 x0) = not (6fb7f.. x0) (proof)
Theorem 44285.. : ∀ x0 : ι → ι → ι . fb516.. x0 ⟶ fb516.. (permargs_i_1_0 x0) (proof)
Theorem 36a9a.. : ∀ x0 x1 : ι → ι → ι . 6fb7f.. x0 ⟶ 6fb7f.. x1 ⟶ 6fb7f.. (cc64c.. x0 x1) (proof)
Theorem b2d00.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ fb516.. (cc64c.. x0 x1) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 72083.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ 6fb7f.. (cc64c.. x0 x1) = and (6fb7f.. x0) (6fb7f.. x1) (proof)
Theorem d266f.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ fb516.. (c2beb.. x0 x1) (proof)
Theorem a5c8f.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ 6fb7f.. (c2beb.. x0 x1) = or (6fb7f.. x0) (6fb7f.. x1) (proof)
Theorem cb82d.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ fb516.. (efcd0.. x0 x1) (proof)
Theorem 72b33.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ 6fb7f.. (efcd0.. x0 x1) = (6fb7f.. x0 ⟶ 6fb7f.. x1) (proof)
Theorem 1fbb5.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ fb516.. (355fd.. x0 x1) (proof)
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Theorem 19010.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ 6fb7f.. (355fd.. x0 x1) = iff (6fb7f.. x0) (6fb7f.. x1) (proof)
Known iff_refl^iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 66636.. : ∀ x0 x1 : ι → ι → ι . fb516.. x0 ⟶ fb516.. x1 ⟶ 6fb7f.. (355fd.. x0 x1) = (x0 = x1) (proof)
Definition f9ee2.. := λ x0 : (ι → ι → ι) → ι → ι → ι . cc64c.. (x0 ChurchBoolTru) (x0 ChurchBoolFal)
Definition 0f571.. := λ x0 : (ι → ι → ι) → ι → ι → ι . c2beb.. (x0 ChurchBoolTru) (x0 ChurchBoolFal)
Theorem 4316e.. : ∀ x0 : (ι → ι → ι) → ι → ι → ι . (∀ x1 : ι → ι → ι . fb516.. x1 ⟶ fb516.. (x0 x1)) ⟶ fb516.. (f9ee2.. x0) (proof)
Theorem ed85c.. : ∀ x0 : (ι → ι → ι) → ι → ι → ι . (∀ x1 : ι → ι → ι . fb516.. x1 ⟶ fb516.. (x0 x1)) ⟶ fb516.. (0f571.. x0) (proof)
Theorem ac245.. : ∀ x0 : (ι → ι → ι) → ι → ι → ι . (∀ x1 : ι → ι → ι . fb516.. x1 ⟶ fb516.. (x0 x1)) ⟶ 6fb7f.. (f9ee2.. x0) = ∀ x2 : ι → ι → ι . fb516.. x2 ⟶ 6fb7f.. (x0 x2) (proof)
Theorem 5030e.. : ∀ x0 : (ι → ι → ι) → ι → ι → ι . (∀ x1 : ι → ι → ι . fb516.. x1 ⟶ fb516.. (x0 x1)) ⟶ 6fb7f.. (0f571.. x0) = ∀ x2 : ο . (∀ x3 : ι → ι → ι . and (fb516.. x3) (6fb7f.. (x0 x3)) ⟶ x2) ⟶ x2 (proof)
Definition 5d5d8.. := λ x0 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x0 ChurchBoolTru ChurchBoolTru
Definition a4575.. := λ x0 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x0 ChurchBoolTru ChurchBoolFal
Definition 17d4e.. := λ x0 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x0 ChurchBoolFal ChurchBoolTru
Definition 79919.. := λ x0 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x0 ChurchBoolFal ChurchBoolFal
Definition 64789.. := λ x0 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (and (x0 = λ x2 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x2 (x0 (λ x3 x4 : ι → ι → ι . x3)) (x0 (λ x3 x4 : ι → ι → ι . x4))) (fb516.. (x0 (λ x1 x2 : ι → ι → ι . x1)))) (fb516.. (x0 (λ x1 x2 : ι → ι → ι . x2)))
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 1f808.. : 64789.. 5d5d8.. (proof)
Theorem c54d8.. : 64789.. a4575.. (proof)
Theorem 3a667.. : 64789.. 17d4e.. (proof)
Theorem 75e29.. : 64789.. 79919.. (proof)
Definition 2a987.. := λ x0 x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . cc64c.. (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x2)) (x1 (λ x2 x3 : ι → ι → ι . x2))) (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x3)) (x1 (λ x2 x3 : ι → ι → ι . x3)))
Definition 36e15.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . f9ee2.. (λ x1 : ι → ι → ι . f9ee2.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2)))
Definition e7e62.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 0f571.. (λ x1 : ι → ι → ι . 0f571.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2)))
Theorem c94f2.. : ∀ x0 x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x0 ⟶ 64789.. x1 ⟶ fb516.. (2a987.. x0 x1) (proof)
Theorem f8400.. : ∀ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ fb516.. (x0 x1)) ⟶ fb516.. (36e15.. x0) (proof)
Theorem a4649.. : ∀ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ fb516.. (x0 x1)) ⟶ fb516.. (e7e62.. x0) (proof)
Theorem 5b3b1.. : ∀ x0 x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x0 ⟶ 64789.. x1 ⟶ 6fb7f.. (2a987.. x0 x1) = (x0 = x1) (proof)
Theorem 3f6be.. : ∀ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ fb516.. (x0 x1)) ⟶ 6fb7f.. (36e15.. x0) = ∀ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x2 ⟶ 6fb7f.. (x0 x2) (proof)
Theorem 0c144.. : ∀ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ fb516.. (x0 x1)) ⟶ 6fb7f.. (e7e62.. x0) = ∀ x2 : ο . (∀ x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x3) (6fb7f.. (x0 x3)) ⟶ x2) ⟶ x2 (proof)
Definition d1ea4.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 5d5d8.. 5d5d8..
Definition 8fca5.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 5d5d8.. a4575..
Definition 96b14.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 5d5d8.. 17d4e..
Definition 759e8.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 5d5d8.. 79919..
Definition 18324.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 a4575.. 5d5d8..
Definition 271f3.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 a4575.. a4575..
Definition f3396.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 a4575.. 17d4e..
Definition 9db64.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 a4575.. 79919..
Definition a9626.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 17d4e.. 5d5d8..
Definition 48d8a.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 17d4e.. a4575..
Definition 1bc5f.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 17d4e.. 17d4e..
Definition c8260.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 17d4e.. 79919..
Definition caa86.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 79919.. 5d5d8..
Definition 856cc.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 79919.. a4575..
Definition f4d2c.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 79919.. 17d4e..
Definition cca5e.. := λ x0 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 79919.. 79919..
Definition 403c9.. := λ x0 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (and (x0 = λ x2 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2 (x0 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x0 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4))) (64789.. (x0 (λ x1 x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x1)))) (64789.. (x0 (λ x1 x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)))
Theorem 74110.. : 403c9.. d1ea4.. (proof)
Theorem 1162a.. : 403c9.. 8fca5.. (proof)
Theorem 812b1.. : 403c9.. 96b14.. (proof)
Theorem bff50.. : 403c9.. 759e8.. (proof)
Theorem 2e578.. : 403c9.. 18324.. (proof)
Theorem 51b07.. : 403c9.. 271f3.. (proof)
Theorem 6ccc7.. : 403c9.. f3396.. (proof)
Theorem 63251.. : 403c9.. 9db64.. (proof)
Theorem b1746.. : 403c9.. a9626.. (proof)
Theorem 7439e.. : 403c9.. 48d8a.. (proof)
Theorem 3bad1.. : 403c9.. 1bc5f.. (proof)
Theorem 873b2.. : 403c9.. c8260.. (proof)
Theorem 3940f.. : 403c9.. caa86.. (proof)
Theorem 305d1.. : 403c9.. 856cc.. (proof)
Theorem e8e54.. : 403c9.. f4d2c.. (proof)
Theorem b08b1.. : 403c9.. cca5e.. (proof)
Definition 86a98.. := λ x0 x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . cc64c.. (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))) (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)))
Definition b1eed.. := λ x0 : (((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 36e15.. (λ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 36e15.. (λ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2)))
Definition fdcb5.. := λ x0 : (((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . e7e62.. (λ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . e7e62.. (λ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2)))
Theorem 8a414.. : ∀ x0 x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x0 ⟶ 403c9.. x1 ⟶ fb516.. (86a98.. x0 x1) (proof)
Theorem 60c3d.. : ∀ x0 : (((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x1 ⟶ fb516.. (x0 x1)) ⟶ fb516.. (b1eed.. x0) (proof)
Theorem 9dd5f.. : ∀ x0 : (((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x1 ⟶ fb516.. (x0 x1)) ⟶ fb516.. (fdcb5.. x0) (proof)
Theorem ee52b.. : ∀ x0 x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x0 ⟶ 403c9.. x1 ⟶ 6fb7f.. (86a98.. x0 x1) = (x0 = x1) (proof)
Theorem 0b5a5.. : ∀ x0 : (((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x1 ⟶ fb516.. (x0 x1)) ⟶ 6fb7f.. (b1eed.. x0) = ∀ x2 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x2 ⟶ 6fb7f.. (x0 x2) (proof)
Theorem e5faa.. : ∀ x0 : (((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ι → ι → ι . (∀ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x1 ⟶ fb516.. (x0 x1)) ⟶ 6fb7f.. (fdcb5.. x0) = ∀ x2 : ο . (∀ x3 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x3) (6fb7f.. (x0 x3)) ⟶ x2) ⟶ x2 (proof)