Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H0: x0 Church10_0 Church10_0.
Assume H1: x0 Church10_0 Church10_1.
Assume H2: x0 Church10_0 Church10_2.
Assume H3: x0 Church10_0 Church10_3.
Assume H4: x0 Church10_0 Church10_4.
Assume H5: x0 Church10_0 Church10_5.
Assume H6: x0 Church10_0 Church10_6.
Assume H7: x0 Church10_0 Church10_7.
Assume H8: x0 Church10_0 Church10_8.
Assume H9: x0 Church10_0 Church10_9.
Assume H10: x0 Church10_1 Church10_0.
Assume H11: x0 Church10_1 Church10_1.
Assume H12: x0 Church10_1 Church10_2.
Assume H13: x0 Church10_1 Church10_3.
Assume H14: x0 Church10_1 Church10_4.
Assume H15: x0 Church10_1 Church10_5.
Assume H16: x0 Church10_1 Church10_6.
Assume H17: x0 Church10_1 Church10_7.
Assume H18: x0 Church10_1 Church10_8.
Assume H19: x0 Church10_1 Church10_9.
Assume H20: x0 Church10_2 Church10_0.
Assume H21: x0 Church10_2 Church10_1.
Assume H22: x0 Church10_2 Church10_2.
Assume H23: x0 Church10_2 Church10_3.
Assume H24: x0 Church10_2 Church10_4.
Assume H25: x0 Church10_2 Church10_5.
Assume H26: x0 Church10_2 Church10_6.
Assume H27: x0 Church10_2 Church10_7.
Assume H28: x0 Church10_2 Church10_8.
Assume H29: x0 Church10_2 Church10_9.
Assume H30: x0 Church10_3 Church10_0.
Assume H31: x0 Church10_3 Church10_1.
Assume H32: x0 Church10_3 Church10_2.
Assume H33: x0 Church10_3 Church10_3.
Assume H34: x0 Church10_3 Church10_4.
Assume H35: x0 Church10_3 Church10_5.
Assume H36: x0 Church10_3 Church10_6.
Assume H37: x0 Church10_3 Church10_7.
Assume H38: x0 Church10_3 Church10_8.
Assume H39: x0 Church10_3 Church10_9.
Assume H40: x0 Church10_4 Church10_0.
Assume H41: x0 Church10_4 Church10_1.
Assume H42: x0 Church10_4 Church10_2.
Assume H43: x0 Church10_4 Church10_3.
Assume H44: x0 Church10_4 Church10_4.
Assume H45: x0 Church10_4 Church10_5.
Assume H46: x0 Church10_4 Church10_6.
Assume H47: x0 Church10_4 Church10_7.
Assume H48: x0 Church10_4 Church10_8.
Assume H49: x0 Church10_4 Church10_9.
Assume H50: x0 Church10_5 Church10_0.
Assume H51: x0 Church10_5 Church10_1.
Assume H52: x0 Church10_5 Church10_2.
Assume H53: x0 Church10_5 Church10_3.
Assume H54: x0 Church10_5 Church10_4.
Assume H55: x0 Church10_5 Church10_5.
Assume H56: x0 Church10_5 Church10_6.
Assume H57: x0 Church10_5 Church10_7.
Assume H58: x0 Church10_5 Church10_8.
Assume H59: x0 Church10_5 Church10_9.
Assume H60: x0 Church10_6 Church10_0.
Assume H61: x0 Church10_6 Church10_1.
Assume H62: x0 Church10_6 Church10_2.
Assume H63: x0 Church10_6 Church10_3.
Assume H64: x0 Church10_6 Church10_4.
Assume H65: x0 Church10_6 Church10_5.
Assume H66: x0 Church10_6 Church10_6.
Assume H67: x0 Church10_6 Church10_7.
Assume H68: x0 Church10_6 Church10_8.
Assume H69: x0 Church10_6 Church10_9.
Assume H70: x0 Church10_7 Church10_0.
Assume H71: x0 ... ....
...
■