Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 1013b.. x0.
Apply unknownprop_5cf7e6965e83150a1907c25d96a0fc30a3e05ee07284c284a3b5f6261ce28afc with λ x1 x2 . 236dc.. (bc82c.. x2 (ce322.. x0)) (bc82c.. (f6a32.. 4a7ef..) (f6a32.. x0)) = x0.
Apply unknownprop_116b1a7b5ba65ca627825e84d83931af55cf809780b181dd0b77c132ec226190 with λ x1 x2 . 236dc.. (bc82c.. 4a7ef.. (ce322.. x0)) (bc82c.. x2 (f6a32.. x0)) = x0.
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 with ce322.. x0, λ x1 x2 . 236dc.. x2 (bc82c.. 4a7ef.. (f6a32.. x0)) = x0 leaving 2 subgoals.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with x0.
The subproof is completed by applying H0.
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 with f6a32.. x0, λ x1 x2 . 236dc.. (ce322.. x0) x2 = x0 leaving 2 subgoals.
Apply unknownprop_29514e25826fa0a942e92f047f92b24dd63fba7537353bf59d9f591e0be2370c with x0.
The subproof is completed by applying H0.
Let x1 of type ιιο be given.
Apply unknownprop_5bfa7e2c4e0c8770e52c317d4111804765880efbe213ccc7f49552da8205fc8a with x0, λ x2 x3 . x1 x3 x2.
The subproof is completed by applying H0.