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: ∀ x3 . prim1 x3 x0x1 x3 = x2 x3.
Let x3 of type ι be given.
Assume H1: prim1 x3 (94f9e.. x0 (λ x4 . x1 x4)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x0, x1, x3, prim1 x3 (94f9e.. x0 x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Assume H2: prim1 x4 x0.
Assume H3: x3 = x1 x4.
Apply H3 with λ x5 x6 . prim1 x6 (94f9e.. x0 (λ x7 . x2 x7)).
Apply H0 with x4, λ x5 x6 . prim1 x6 (94f9e.. x0 (λ x7 . x2 x7)) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with x0, x2, x4.
The subproof is completed by applying H2.