Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: atleastp (setsum 0 6a551..) 0.
Apply unknownprop_7963a4bf2feda239add5cf25163811bc2206f6f21a0e4a70277699970e74fa1e with setsum 0 6a551.., 0, False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι → ι be given.
Assume H1: inj (setsum 0 6a551..) 0 x3.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with setsum 0 6a551.., 0, x3, False leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: ∀ x4 . In x4 (setsum 0 6a551..) ⟶ In (x3 x4) 0.
Assume H3: ∀ x4 . In x4 (setsum 0 6a551..) ⟶ ∀ x5 . In x5 (setsum 0 6a551..) ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x3 (Inj1 0).
Apply H2 with Inj1 0.
Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with 0, 6a551.., 0.
The subproof is completed by applying unknownprop_8285cfa4fcfced8bf8f28f246aaeb081e0d4a211d67c239e326650337a8e69c8 with 99f52...
■