Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: ba9d8.. x2.
Assume H1: prim1 x1 (prim0 (aa8d2.. x2 x0)).
Apply UnionI with 94f9e.. 48ef8.. (λ x3 . prim0 (aa8d2.. x3 x0)), x1, prim0 (aa8d2.. x2 x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with 48ef8.., λ x3 . prim0 (aa8d2.. x3 x0), x2.
Apply unknownprop_b67f6d586fb9d8883c38540f89ba210beeb3fabc8048f066af6580d3cbff51ec with x2.
The subproof is completed by applying H0.