Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply unknownprop_d5fe081172aba4c6b837c605e81895e596299f90a3c175e299a62d6301b84787 with f6917.. x0, λ x1 x2 . x2 = x0.
Apply set_ext with 94f9e.. (1ad11.. (f6917.. x0) (91630.. 4a7ef..)) (λ x1 . 158d3.. x1), x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0: prim1 x1 (94f9e.. (1ad11.. (f6917.. x0) (91630.. 4a7ef..)) (λ x2 . 158d3.. x2)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with 1ad11.. (f6917.. x0) (91630.. 4a7ef..), 158d3.., x1, prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1: prim1 x2 (1ad11.. (f6917.. x0) (91630.. 4a7ef..)).
Assume H2: x1 = 158d3.. x2.
Apply unknownprop_b29d0d66991b8737c3ef6109cea8b8736c6edd642ea721f35cfa04fecdda0905 with f6917.. x0, 91630.. 4a7ef.., x2, prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: prim1 x2 (94f9e.. x0 (λ x3 . 09364.. x3)).
Assume H4: nIn x2 (91630.. 4a7ef..).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x0, 09364.., x2, prim1 x1 x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H5: prim1 x3 x0.
Assume H6: x2 = 09364.. x3.
Claim L7: x1 = x3
Apply H2 with λ x4 x5 . x5 = x3.
Apply H6 with λ x4 x5 . 158d3.. x5 = x3.
The subproof is completed by applying unknownprop_220466dabb9c90c9b087796465f1368ac3c1e9d1ef55643ebed4c27316fb8803 with x3.
Apply L7 with λ x4 x5 . prim1 x5 x0.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Assume H0: prim1 x1 x0.
Apply unknownprop_220466dabb9c90c9b087796465f1368ac3c1e9d1ef55643ebed4c27316fb8803 with x1, λ x2 x3 . prim1 x2 (94f9e.. (1ad11.. (f6917.. x0) (91630.. 4a7ef..)) (λ x4 . 158d3.. x4)).
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with 1ad11.. (f6917.. x0) (91630.. 4a7ef..), 158d3.., 09364.. x1.
Apply unknownprop_4469442df960b88f16925ae745a59dde3c3d26a1d7b003702e92e0a7ea2361ef with f6917.. x0, 91630.. 4a7ef.., 09364.. x1 leaving 2 subgoals.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with x0, 09364.., x1.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_7b335352103c79ef49f754be56d252f529fd8e1668f95cb6d3292ed9a0f32342 with x1.