Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u13.
Let x1 of type ο be given.
Apply unknownprop_713be0ad5efeb9da26a66462505f19060bd4cc2891c0c4c304dba8053e47660a with x0, λ x2 . (∀ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x3 ⟶ x2 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1) ⟶ x1 leaving 14 subgoals.
The subproof is completed by applying H0.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ 0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_a619d41e7dd73fd2fd7a22e345cc585bca94f0a556dabdde7ba613d280fc1bb9.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 0 0.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ u1 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_56e5b078b135657df6b920f8c41633bbbc869255cbf04817b1c0569e953798ea.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u1 u1.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ u2 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_64a05e04ff07f2333eab12fcce0b713bfb051cbbce19306572d78b255c2f5222.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u2 u2.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ u3 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x5 leaving 2 subgoals.
The subproof is completed by applying unknownprop_ccf2dc8baa5a60239d2b334119b91cb320d200e197fef0daa6705ddcacfec32a.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u3 u3.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ u4 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x6 leaving 2 subgoals.
The subproof is completed by applying unknownprop_ec3bfa3241ab3c5244e2af2ff034529622ae6db8f50ffa68a44651955e5adb06.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u4 u4.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ u5 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x7 leaving 2 subgoals.
The subproof is completed by applying unknownprop_2275c30730a86a8b5e92c69a3cf62226cb91c94f842745d885aae952e4aec475.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u5 u5.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ u6 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x8 leaving 2 subgoals.
The subproof is completed by applying unknownprop_af2a1b54824c0bcac106e306823cdf745ddadb1cb4ff3d16a82269625fefc7d4.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 u6 u6.
The subproof is completed by applying H2.
Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ u7 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1.
Apply H1 with λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x9 leaving 2 subgoals.
The subproof is completed by applying unknownprop_596dfb802632adb73ea48164c53a57c30f1012fe27955d11686758a101b7149d.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 ... ....
...
...
...
...
...
...
■