Claim L0: ((λ x0 x1 . x1) = λ x0 x1 . x0) ⟶ ∀ x0 : ο . x0
The subproof is completed by applying unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
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 . x3) ⟶ (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 . x3) ⟶ (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 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x3 x4 . x3) ⟶ 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_ff49046eea45e52be0679da7e60a06faabb9bec19c71965e127e54eb9539f5f3 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.
The subproof is completed by applying H4.
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_354b4f1f97bbb4f2cdb2200623d77e815b98a25ce80df80b154c7f787661debc 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.
The subproof is completed by applying H4.