Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Let x1 of type ο be given.
Assume H1: ∀ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (x0 = ad280.. x2 x3))x1.
Apply H1 with x0.
Apply andI with SNo x0, ∃ x2 . and (SNo x2) (x0 = ad280.. x0 x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ο be given.
Assume H2: ∀ x3 . and (SNo x3) (x0 = ad280.. x0 x3)x2.
Apply H2 with 0.
Apply andI with SNo 0, x0 = ad280.. x0 0 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Let x3 of type ιιο be given.
The subproof is completed by applying unknownprop_872273e895264b163d3a3b042c5d1abf262e26919401a643ccce2dcdcb6a14ef with x0, λ x4 x5 . x3 x5 x4.