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.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Apply unknownprop_0061f7d7cc7224d66e31f046473573b0f6090fa03a4a5550b0992c7403d46f83 with x0, x2, λ x4 x5 . 40dde.. x5 (λ x6 . prim1 x6 (09072.. x0 x2)) (e4431.. (09072.. x1 x3)) (λ x6 . prim1 x6 (09072.. x1 x3))40dde.. x0 x2 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_0061f7d7cc7224d66e31f046473573b0f6090fa03a4a5550b0992c7403d46f83 with x1, x3, λ x4 x5 . 40dde.. x0 (λ x6 . prim1 x6 (09072.. x0 x2)) x5 (λ x6 . prim1 x6 (09072.. x1 x3))40dde.. x0 x2 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: 40dde.. x0 (λ x4 . prim1 x4 (09072.. x0 x2)) x1 (λ x4 . prim1 x4 (09072.. x1 x3)).
Apply unknownprop_516ec77a0547bdde87f302357c77a8c500e4737d03bed523bd783f1c87c1572b with x0, x1, x2, λ x4 . prim1 x4 (09072.. x0 x2), x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply PNoEq_sym_ with x0, λ x4 . prim1 x4 (09072.. x0 x2), x2.
Apply unknownprop_8ab8782df8e80eb287fd4c918f7b35b584f8954d0de002e6915e8d87848fc5f4 with x0, x2.
The subproof is completed by applying H0.
Apply unknownprop_8400f668ce579075dd52a6b0bc8eaa2c816f68129d64497b65439b55d60266f7 with x0, x1, λ x4 . prim1 x4 (09072.. x0 x2), λ x4 . prim1 x4 (09072.. x1 x3), x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_8ab8782df8e80eb287fd4c918f7b35b584f8954d0de002e6915e8d87848fc5f4 with x1, x3.
The subproof is completed by applying H1.