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.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply unknownprop_b456609235d152f08bccfce314d541d7c44f3716137c00b0ce21cf467ba83d17 with 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))), λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))), 4ae4a.. 4a7ef.., λ x6 x7 . x7 = x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_fe74110dcead2d1e188589477df709ee185db600278b9e4d137b4ce4b8ce241c.
Apply If_i_0 with 4ae4a.. 4a7ef.. = 4a7ef.., x0, If_i (4ae4a.. 4a7ef.. = 4ae4a.. 4a7ef..) x1 (If_i (4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5))), λ x6 x7 . x7 = x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_24ff2ea632296eb0012bd83ffdc0e75761169422164b438efe0673b96d912be0.
Apply If_i_1 with 4ae4a.. 4a7ef.. = 4ae4a.. 4a7ef.., x1, If_i (4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)).
Let x6 of type ι → ι → ο be given.
Assume H0: x6 (4ae4a.. 4a7ef..) (4ae4a.. 4a7ef..).
The subproof is completed by applying H0.
■