Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιο be given.
Assume H0: x0 c4def...
Assume H1: ∀ x1 x2 . x0 x1x0 x2x0 (6b90c.. x1 x2).
Assume H2: x0 c9248...
Assume H3: ∀ x1 . x0 x1x0 (a6e19.. x1).
Assume H4: ∀ x1 . x0 x1x0 (2fe34.. x1).
Assume H5: ∀ x1 x2 . x0 x1x0 x2x0 (3e00e.. x1 x2).
Assume H6: ∀ x1 x2 . x0 x1x0 x2x0 (f9341.. x1 x2).
Assume H7: ∀ x1 . x0 x1x0 (1fa6d.. x1).
Assume H8: ∀ x1 . x0 x1x0 (3a365.. x1).
The subproof is completed by applying H0.