Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . 9f253.. x0struct_u x0
Let x0 of type ι be given.
Assume H0: 9f253.. x0.
Apply H0 with struct_u x0.
Assume H1: struct_u x0.
Assume H2: unpack_u_o x0 (λ x1 . λ x2 : ι → ι . ∀ x3 . x3x1x2 (x2 x3) = x2 x3).
The subproof is completed by applying H1.
Apply unknownprop_137f848bdb78f472068da9f3e5698255d8403888e1b30f209fd7da0af03ad2f1 with 9f253...
The subproof is completed by applying L0.