Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)).
Apply unknownprop_285d1412c16abfd3320f0ee89e600fad3199271183754290c3d7bd1f86d5a491 with x0, λ x1 . bd0b9.. x1 ⟶ x1 = 4ae4a.. 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: bd0b9.. 4a7ef...
Apply FalseE with 4a7ef.. = 4ae4a.. 4a7ef...
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with 4a7ef...
The subproof is completed by applying H1.
Assume H1: bd0b9.. (4ae4a.. 4a7ef..).
Let x1 of type ι → ι → ο be given.
Assume H2: x1 (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..).
The subproof is completed by applying H2.
■