Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u6.
Let x1 of type ι be given.
Assume H1: x1 ∈ u6.
Let x2 of type ι be given.
Assume H2: x2 ∈ u6.
Let x3 of type ι be given.
Assume H3: x3 ∈ u6.
Assume H4: TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x4 x5 . x4.
Apply unknownprop_47da0888016e4abdf776e90f0c4d8acdbc20378a540bacd2cfd7afa4885f61a8 with nth_6_tuple x0, nth_6_tuple x1, nth_6_tuple x2, nth_6_tuple x3 leaving 5 subgoals.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x0.
The subproof is completed by applying H0.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x1.
The subproof is completed by applying H1.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x2.
The subproof is completed by applying H2.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x3.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
■