Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι(ιιι) → (ιιι) → CT2 ι be given.
Let x1 of type ι be given.
Let x2 of type ιιι be given.
Let x3 of type ιιι be given.
Let x4 of type ιιι be given.
Assume H0: ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1∀ x7 . prim1 x7 x1x2 x6 x7 = x5 x6 x7)∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1x3 x7 x8 = x6 x7 x8)∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1∀ x9 . prim1 x9 x1x4 x8 x9 = x7 x8 x9)x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4.
Apply unknownprop_8f65da788a93ff89d95bcf516abc29daa711f2c16faefefcaad5ba81f2e71786 with x1, x2, x3, x4, λ x5 x6 . x0 x5 (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4.
Apply H0 with e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. 4a7ef..)), e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))), e3162.. (f482f.. (7c612.. x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 3 subgoals.
The subproof is completed by applying unknownprop_ff4535e6de7d81b5e64319b54276975d755c6038dfc6568b8eaad6de9e67f064 with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_d91c9a6f9c15a2c6b9d2b80e56f063e4e1af105da6d9f1d5f7ab2c269bb9687a with x1, x2, x3, x4.
The subproof is completed by applying unknownprop_d90cbda69461be2219583389e1055578190fbc4e0c943c03394d871429ab3a0a with x1, x2, x3, x4.