Claim L0: ((λ x0 x1 . x0) = λ x0 x1 . x1) ⟶ ∀ x0 : ο . x0
Assume H0: (λ x0 x1 . x0) = λ x0 x1 . x1.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
Let x0 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H0 with λ x1 x2 : ι → ι → ι . x0 x2 x1.
Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x2 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply unknownprop_1030b2f82370682da82bd2e49c05e6c78943595f102389be16df3b42b6279cb8 with
x0,
((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x0 = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x1 = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3) x2 = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x3 x4 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x3 x4 . x4) ⟶ False leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H4: (λ x3 x4 . x0 x3 x3 x3 x3 x3 x3 x3 x3 x3 x4 x4 x4 x4 x4 x4 x4 x4) = λ x3 x4 . x3.
Apply unknownprop_1f2bba689392703fd9ae4d43bb1fb4db9f6cb380e2866ddb66d73f17c1bb7937 with
x0,
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x3 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H4 with λ x4 x5 : ι → ι → ι . x3 x5 x4.
Assume H4: (λ x3 x4 . x0 x4 x4 x4 x4 x4 x4 x4 x4 x4 x3 x3 x3 x3 x3 x3 x3 x3) = λ x3 x4 . x3.
Apply unknownprop_0c179d13b0842b8b667bad141e154df467dcf4161461e0e5d6153322ede94224 with
x0,
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x3 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
The subproof is completed by applying H4 with λ x4 x5 : ι → ι → ι . x3 x5 x4.