Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with λ x0 . bc82c.. 4a7ef.. x0 = x0.
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: ∀ x1 . prim1 x1 (56ded.. (e4431.. x0)) ⟶ bc82c.. 4a7ef.. x1 = x1.
Apply unknownprop_b2d3cb96a6a882d02e5e57dcfc02559b580d1f8621959f82afe70dc68a4b010f with 4a7ef.., x0, λ x1 x2 . x2 = x0 leaving 3 subgoals.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
The subproof is completed by applying H0.
Claim L2: 0ac37.. (94f9e.. (23e07.. 4a7ef..) (λ x1 . bc82c.. x1 x0)) (94f9e.. (23e07.. x0) (λ x1 . bc82c.. 4a7ef.. x1)) = 23e07.. x0
Apply unknownprop_f4186be5e162d2897dfc606cffae37f597510b883639ada8195c8b9cd6dcf94c with λ x1 x2 . 0ac37.. (94f9e.. x2 (λ x3 . bc82c.. x3 x0)) (94f9e.. (23e07.. x0) (λ x3 . bc82c.. 4a7ef.. x3)) = 23e07.. x0.
Apply unknownprop_cad282ef0fdd0498b9d72e39ef4bede1603c0487cbba81dcc7e691931f33d73a with λ x1 . bc82c.. x1 x0, λ x1 x2 . 0ac37.. x2 (94f9e.. (23e07.. x0) (λ x3 . bc82c.. 4a7ef.. x3)) = 23e07.. x0.
...
Claim L3: 0ac37.. (94f9e.. (5246e.. 4a7ef..) (λ x1 . bc82c.. x1 x0)) (94f9e.. (5246e.. x0) (λ x1 . bc82c.. 4a7ef.. x1)) = 5246e.. x0
Apply unknownprop_897b65b5b24b1c74f33d6c2cd6cfb0aac2c01f465a9fd9938139f0409ef66fcc with λ x1 x2 . 0ac37.. (94f9e.. x2 (λ x3 . bc82c.. x3 x0)) (94f9e.. (5246e.. x0) (λ x3 . bc82c.. 4a7ef.. x3)) = 5246e.. x0.
Apply unknownprop_cad282ef0fdd0498b9d72e39ef4bede1603c0487cbba81dcc7e691931f33d73a with λ x1 . bc82c.. x1 x0, λ x1 x2 . 0ac37.. x2 (94f9e.. (5246e.. x0) (λ x3 . bc82c.. 4a7ef.. x3)) = 5246e.. x0.
Apply unknownprop_fc17ae1257247ccbad94ae05ce6b26282126a44d809f22e0209b526a567506af with 94f9e.. (5246e.. x0) (λ x1 . bc82c.. 4a7ef.. x1), λ x1 x2 . x2 = 5246e.. x0.
Apply set_ext with 94f9e.. (5246e.. x0) (λ x1 . bc82c.. 4a7ef.. x1), 5246e.. x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H3: prim1 x1 (94f9e.. (5246e.. x0) (λ x2 . bc82c.. 4a7ef.. x2)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with 5246e.. x0, λ x2 . bc82c.. 4a7ef.. x2, x1, prim1 x1 (5246e.. x0) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: prim1 x2 (5246e.. x0).
Assume H5: x1 = bc82c.. 4a7ef.. x2.
Apply H5 with λ x3 x4 . prim1 x4 (5246e.. x0).
Apply H1 with x2, λ x3 x4 . prim1 x4 (5246e.. x0) leaving 2 subgoals.
Apply unknownprop_cd4082b132eebd1418f67184106c9cd974b71dcdba0a1c046b254bc4ec1b1cd5 with x0, x2.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H3: prim1 x1 (5246e.. x0).
Apply H1 with x1, λ x2 x3 . prim1 x2 (94f9e.. (5246e.. x0) (λ x4 . bc82c.. 4a7ef.. x4)) leaving 2 subgoals.
Apply unknownprop_cd4082b132eebd1418f67184106c9cd974b71dcdba0a1c046b254bc4ec1b1cd5 with x0, x1.
The subproof is completed by applying H3.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with 5246e.. x0, λ x2 . bc82c.. 4a7ef.. x2, x1.
The subproof is completed by applying H3.
Apply L2 with λ x1 x2 . 02a50.. x2 (0ac37.. (94f9e.. (5246e.. 4a7ef..) (λ x3 . bc82c.. x3 x0)) (94f9e.. (5246e.. x0) (λ x3 . bc82c.. 4a7ef.. x3))) = x0.
Apply L3 with λ x1 x2 . 02a50.. (23e07.. x0) x2 = x0.
Let x1 of type ι → ι → ο be given.
Apply unknownprop_5eea512ff6a0660b21c1b66a95dd1433034b1476627ffa8d2700dd808eef5a0c with x0, λ x2 x3 . x1 x3 x2.
The subproof is completed by applying H0.
■