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_b7caf5f70ae79c72282a4433b7742206b9e82c71b0701b7f8019ceccbdfb80a7 with x0, x1, 02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (λ x2 . bc82c.. x0 x2))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (λ x2 . bc82c.. x0 x2))) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2: and (and (and (and (80242.. (bc82c.. x0 x1)) (∀ x2 . prim1 x2 (23e07.. x0)099f3.. (bc82c.. x2 x1) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x0)099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1))) (∀ x2 . prim1 x2 (23e07.. x1)099f3.. (bc82c.. x0 x2) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x1)099f3.. (bc82c.. x0 x1) (bc82c.. x0 x2)).
Assume H3: 02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0))).
The subproof is completed by applying H3.