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: prim1 x2 (a4c2a.. x0 (λ x3 . ∃ x4 . x3 = aae7a.. x1 x4) (λ x3 . 22ca9.. x3)).
Apply unknownprop_e546e9a8cc28c7314a8604ada98e2a83641f2ef6b8078441570ffe037b28d26f with x0, λ x3 . ∃ x4 . x3 = aae7a.. x1 x4, 22ca9.., x2, prim1 (aae7a.. x1 x2) x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H1: prim1 x3 x0.
Assume H2: ∃ x4 . x3 = aae7a.. x1 x4.
Assume H3: x2 = 22ca9.. x3.
Apply H2 with prim1 (aae7a.. x1 x2) x0.
Let x4 of type ι be given.
Assume H4: x3 = aae7a.. x1 x4.
Claim L5: x2 = x4
Apply H3 with λ x5 x6 . x6 = x4.
Apply H4 with λ x5 x6 . 22ca9.. x6 = x4.
The subproof is completed by applying unknownprop_916f469d850241375b1e44b2c6308f0113078869ceee129c02712fae69c32a37 with x1, x4.
Claim L6: x3 = aae7a.. x1 x2
Apply L5 with λ x5 x6 . x3 = aae7a.. x1 x6.
The subproof is completed by applying H4.
Apply L6 with λ x5 x6 . prim1 x5 x0.
The subproof is completed by applying H1.