Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_2c926b240fc658005337215abfdc8124a6f6eea17ba9f4df80d254bab3845972 with λ x2 x3 : ι → ι → ο . (∀ x4 . In x4 x1∃ x5 . and (In x5 x0) (∃ x6 . x4 = setsum x5 x6))x3 x0 x1.
Assume H0: ∀ x2 . In x2 x1∃ x3 . and (In x3 x0) (∃ x4 . x2 = setsum x3 x4).
The subproof is completed by applying H0.