Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Apply unknownprop_54bb640991f3dc5ef625d0dd80688a536de93bc223668dfbefbc6eb5651b1208 with x0, x1, 80242.. (e6316.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2: 80242.. (e6316.. x0 x1).
Assume H3: ∀ x2 . prim1 x2 (23e07.. x0) ⟶ ∀ x3 . prim1 x3 (23e07.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x2 x1) (e6316.. x0 x3)) (bc82c.. (e6316.. x0 x1) (e6316.. x2 x3)).
Assume H4: ∀ x2 . prim1 x2 (5246e.. x0) ⟶ ∀ x3 . prim1 x3 (5246e.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x2 x1) (e6316.. x0 x3)) (bc82c.. (e6316.. x0 x1) (e6316.. x2 x3)).
Assume H5: ∀ x2 . prim1 x2 (23e07.. x0) ⟶ ∀ x3 . prim1 x3 (5246e.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x0 x1) (e6316.. x2 x3)) (bc82c.. (e6316.. x2 x1) (e6316.. x0 x3)).
Assume H6: ∀ x2 . prim1 x2 (5246e.. x0) ⟶ ∀ x3 . prim1 x3 (23e07.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x0 x1) (e6316.. x2 x3)) (bc82c.. (e6316.. x2 x1) (e6316.. x0 x3)).
The subproof is completed by applying H2.
■